1.1 --- a/doc-isac/jrocnik/Test_Complex.thy	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/doc-isac/jrocnik/Test_Complex.thy	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -24,9 +24,9 @@
     1.4  
     1.5  ML {*
     1.6  val a = @{term "Complex 1 2"};
     1.7 -atomty a;
     1.8 +TermC.atom_trace_detail @{context} a;
     1.9  val a = TermC.parse_test @{context} "Complex 1 2";
    1.10 -atomty a;
    1.11 +TermC.atom_trace_detail @{context} a;
    1.12  *}
    1.13  ML {*
    1.14  val b = @{term "Complex 3 4"};
    1.15 @@ -68,7 +68,7 @@
    1.16  
    1.17  val t = TermC.parse_test @{context} "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
    1.18  term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
    1.19 -atomty t;
    1.20 +TermC.atom_trace_detail @{context} t;
    1.21  
    1.22  *}
    1.23  ML {*
    1.24 @@ -77,7 +77,7 @@
    1.25  val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    1.26  
    1.27  term2str t = "Complex -12 26";
    1.28 -atomty t;
    1.29 +TermC.atom_trace_detail @{context} t;
    1.30  
    1.31  *}
    1.32  
    1.33 @@ -92,14 +92,14 @@
    1.34  ML {*
    1.35  val t = TermC.parse_test @{context} "inverse (Complex (2::real) (4::real))";
    1.36  term2str t = "inverse Complex (2) (4)";
    1.37 -atomty t;
    1.38 +TermC.atom_trace_detail @{context} t;
    1.39  *}
    1.40  ML {*
    1.41  trace_rewrite := true;
    1.42  val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    1.43  trace_rewrite := false;
    1.44  term2str t = "Complex -12 26";
    1.45 -atomty t;
    1.46 +TermC.atom_trace_detail @{context} t;
    1.47  *}
    1.48  
    1.49  

     2.1 --- a/doc-isac/mat-eng-de.tex	Wed Jan 11 09:23:18 2023 +0100
     2.2 +++ b/doc-isac/mat-eng-de.tex	Wed Jan 11 11:38:01 2023 +0100
     2.3 @@ -97,9 +97,9 @@
     2.4              (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
     2.5                 ...) : Term.term
     2.6  \end{verbatim}}
     2.7 -Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt atomty} \"ubergeben werden, die diesen in einer dritten Form zeigt:
     2.8 +Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt TermC.atom_trace_detail @{context}} \"ubergeben werden, die diesen in einer dritten Form zeigt:
     2.9  {\footnotesize\begin{verbatim}
    2.10 -   > atomty term;
    2.11 +   > TermC.atom_trace_detail \@\{context\} term;
    2.12   
    2.13     ***
    2.14     *** Const (op +, [real, real] => real)
    2.15 @@ -288,7 +288,7 @@
    2.16           Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
    2.17           Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
    2.18       : Theory.theory
    2.19 -   > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    2.20 +   > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    2.21   
    2.22        ***
    2.23        *** Free (d_d, [real, real] => real)
    2.24 @@ -316,7 +316,7 @@
    2.25           Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
    2.26           PolyEq, LogExp, Diff} : Theory.theory
    2.27   
    2.28 -   > ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    2.29 +   > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    2.30   
    2.31        ***
    2.32        *** Const (Diff.d_d, [real, real] => real)
    2.33 @@ -581,11 +581,11 @@
    2.34  "\n"
    2.35  val it = "\n" : string
    2.36  \end{verbatim}}
    2.37 -Das Modell wird durch den Befehl \textit{free2var} erstellt.
    2.38 +Das Modell wird durch den Befehl \textit{mk_Var} erstellt.
    2.39  {\footnotesize\begin{verbatim}
    2.40 -> free2var;
    2.41 +> mk_Var;
    2.42  val it = fn : Term.term -> Term.term
    2.43 -> val pat = free2var p;
    2.44 +> val pat = mk_Var p;
    2.45  val pat =
    2.46  Const ("op =", "[RealDef.real, RealDef.real] => bool") $
    2.47  (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $

     3.1 --- a/doc-isac/mat-eng-en.tex	Wed Jan 11 09:23:18 2023 +0100
     3.2 +++ b/doc-isac/mat-eng-en.tex	Wed Jan 11 11:38:01 2023 +0100
     3.3 @@ -216,9 +216,9 @@
     3.4     *** . . Free ( #3, )
     3.5     val it = () : unit
     3.6     ML>
     3.7 -   ML> atomty;
     3.8 +   ML> TermC.atom_trace_detail \@\{context\};
     3.9     val it = fn : theory -> term -> unit
    3.10 -   ML> atomty thy t;
    3.11 +   ML> TermC.atom_trace_detail \@\{context\} t;
    3.12     *** -------------
    3.13     *** Const ( op +, [real, real] => real)
    3.14     *** . Free ( a, real)
    3.15 @@ -255,7 +255,7 @@
    3.16  Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots
    3.17  {\footnotesize\begin{verbatim}
    3.18     ML> (*-4-*) val thy = RatArith.thy;
    3.19 -   ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    3.20 +   ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    3.21     *** -------------
    3.22     *** Free ( d_d, [real, real] => real)
    3.23     *** . Free ( x, real)
    3.24 @@ -265,7 +265,7 @@
    3.25     val it = () : unit
    3.26     ML>
    3.27     ML> (*-6-*) val thy = Differentiate.thy;
    3.28 -   ML> ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    3.29 +   ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
    3.30     *** -------------
    3.31     *** Const ( Differentiate.d_d, [real, real] => real)
    3.32     *** . Free ( x, real)
    3.33 @@ -866,10 +866,10 @@
    3.34     *** . Free ( c, )
    3.35     val it = () : unit
    3.36     ML>
    3.37 -   ML> free2var;
    3.38 +   ML> mk_Var;
    3.39     val it = fn : term -> term
    3.40     ML>
    3.41 -   ML> val pat = free2var p;
    3.42 +   ML> val pat = mk_Var p;
    3.43     val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
    3.44     ML> Sign.string_of_term (sign_of thy) pat;
    3.45     val it = "?a * ?b ^^^ #2 = ?c" : cterm' 
    3.46 @@ -884,7 +884,7 @@
    3.47     *** . Var ((c, 0), )
    3.48     val it = () : unit
    3.49  \end{verbatim}}%size % $ 
    3.50 -Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt free2var}. This format of the pattern is necessary in order to obtain results like these:
    3.51 +Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt mk_Var}. This format of the pattern is necessary in order to obtain results like these:
    3.52  {\footnotesize\begin{verbatim}
    3.53     ML> matches thy t pat;
    3.54     val it = true : bool

     4.1 --- a/doc-isac/mat-eng.sml	Wed Jan 11 09:23:18 2023 +0100
     4.2 +++ b/doc-isac/mat-eng.sml	Wed Jan 11 11:38:01 2023 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  TermC.parse_test @{context} "a + b * 3";
     4.5  val term = TermC.parse_test @{context} "a + b * 3";
     4.6  atomt term;
     4.7 -atomty term;
     4.8 +TermC.atom_trace_detail @{context} term;
     4.9  
    4.10  (*2.3. Theories and parsing*)
    4.11  
    4.12 @@ -92,7 +92,7 @@
    4.13       Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
    4.14       Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
    4.15  : Theory.theory
    4.16 -> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.17 +> ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.18  
    4.19  ***
    4.20  *** Free (d_d, [real, real] => real)
    4.21 @@ -118,7 +118,7 @@
    4.22       Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
    4.23       PolyEq, LogExp, Diff} : Theory.theory
    4.24  
    4.25 -> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.26 +> ((TermC.atom_trace_detail @{context}) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.27  
    4.28  ***
    4.29  *** Const (Diff.d_d, [real, real] => real)
    4.30 @@ -176,8 +176,8 @@
    4.31   ?Compiler.Control.Print.stringDepth;
    4.32   atomt;
    4.33   atomt t; 
    4.34 - atomty;
    4.35 - atomty thy t;
    4.36 + TermC.atom_trace_detail @{context};
    4.37 + TermC.atom_trace_detail @{context} t;
    4.38  (*Give it a try: the mathematics knowledge grows*)
    4.39   parse HOL.thy "2^^^3";
    4.40   parse HOL.thy "d_d x (a + x)";
    4.41 @@ -187,9 +187,9 @@
    4.42   ?parse Differentiate.thy "#2^^^#3";
    4.43  (*don't trust the string representation*)
    4.44   ?val thy = RatArith.thy;
    4.45 - ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.46 + ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.47   ?val thy = Differentiate.thy;
    4.48 - ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.49 + ((TermC.atom_trace_detail @{context} thy) o term_of o the o (parse thy)) "d_d x (a + x)";
    4.50  
    4.51  (*2.4. Converting terms*)
    4.52   term_of;
    4.53 @@ -384,8 +384,8 @@
    4.54   val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
    4.55   val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
    4.56   atomt p;
    4.57 - free2var;
    4.58 - val pat = free2var p;
    4.59 + mk_Var;
    4.60 + val pat = mk_Var p;
    4.61   matches thy t pat;
    4.62  
    4.63   val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";

     5.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 09:23:18 2023 +0100
     5.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 11:38:01 2023 +0100
     5.3 @@ -85,7 +85,6 @@
     5.4    val str_of_int: int -> string
     5.5    val strip_imp_prems': term -> term option
     5.6    val subst_atomic_all: LibraryC.subst -> term -> bool * term
     5.7 -  val term_detail2str: term -> string
     5.8  
     5.9    val pairt: term -> term -> term
    5.10    val pairT: typ -> typ -> typ
    5.11 @@ -103,19 +102,19 @@
    5.12    val contains_Const_typeless: term list -> term -> bool
    5.13    val sym_trm : term -> term (* unused code, kept as hints to design ideas *)
    5.14  
    5.15 -(*isac_test*)
    5.16 +  val string_of_detail: Proof.context -> term -> string
    5.17 +
    5.18 +\<^isac_test>\<open>
    5.19    val mk_negative: typ -> term -> term
    5.20 -  val free2var: term -> term
    5.21 +  val mk_Var: term -> term
    5.22    val scala_of_term: term -> string
    5.23  
    5.24 -(*val atom_typ: typ -> unit RENAME*)
    5.25 -  val atomtyp: typ -> unit
    5.26 -  val atomty: term -> unit
    5.27 -  val atomw: term -> unit
    5.28 -  val atomt: term -> unit
    5.29 -  val atomwy: term -> unit
    5.30 +  val atom_typ: Proof.context -> typ -> unit
    5.31 +  val atom_write: Proof.context -> term -> unit
    5.32 +  val atom_trace: Proof.context -> term -> unit
    5.33  
    5.34 -\<^isac_test>\<open>
    5.35 +  val atom_write_detail: Proof.context -> term -> unit
    5.36 +  val atom_trace_detail: Proof.context -> term -> unit
    5.37  \<close>
    5.38  end
    5.39  
    5.40 @@ -151,7 +150,20 @@
    5.41      handle Pattern.MATCH => false
    5.42  
    5.43  (** transform  typ / term to a String to be parsed by Scala after transport via libisabelle **)
    5.44 -(*isac_test*)
    5.45 +fun string_of_detail ctxt t =
    5.46 +  let
    5.47 +    fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    5.48 +      | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    5.49 +      | ato (Var ((a, i), T)) n =
    5.50 +        "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    5.51 +      | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
    5.52 +      | ato (Abs(a, T, body))  n = 
    5.53 +        "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1)
    5.54 +      | ato (f $ t) n = ato f n ^ ato t (n + 1)
    5.55 +  in "\n*** " ^ ato t 0 ^ "\n***" end;
    5.56 +
    5.57 +
    5.58 +\<^isac_test>\<open>
    5.59  fun scala_of_typ (Type (s, typs)) =
    5.60      enclose "Type(" ")" (quote s ^ ", " ^
    5.61        (typs |> map scala_of_typ |> commas |> enclose "List(" ")"))
    5.62 @@ -181,7 +193,7 @@
    5.63  
    5.64  (* see structure's bare bones.
    5.65     for Isabelle standard output compare 2017 "structure ML_PP" *)
    5.66 -fun atomtyp t =
    5.67 +fun atom_typ ctxt t =
    5.68    let
    5.69      fun ato n (Type (s, [])) = "\n*** " ^ indent n ^ "Type (" ^ s ^",[])"
    5.70        | ato n (Type (s, Ts)) = "\n*** " ^ indent n ^ "Type (" ^ s ^ ",[" ^ atol (n + 1) Ts
    5.71 @@ -201,31 +213,12 @@
    5.72  	  | ato (Abs (a, _, body)) n = "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
    5.73  	  | ato (f $ t) n = (ato f n ^ ato t (n + 1))
    5.74  in
    5.75 -  fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
    5.76 -  fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
    5.77 +  fun atom_write _ t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
    5.78 +  fun atom_trace _ t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
    5.79  end;
    5.80  
    5.81 -\<^isac_test>\<open>
    5.82 -\<close>
    5.83 -
    5.84 -fun term_detail2str t =
    5.85 -  let
    5.86 -    val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global
    5.87 -    fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    5.88 -      | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    5.89 -      | ato (Var ((a, i), T)) n =
    5.90 -        "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    5.91 -      | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
    5.92 -      | ato (Abs(a, T, body))  n = 
    5.93 -        "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1)
    5.94 -      | ato (f $ t) n = ato f n ^ ato t (n + 1)
    5.95 -  in "\n*** " ^ ato t 0 ^ "\n***" end;
    5.96 -
    5.97 -(*isac_test*)
    5.98 -fun atomwy t = (writeln o term_detail2str) t;
    5.99 -fun atomty t = (tracing o term_detail2str) t;
   5.100 -
   5.101 -\<^isac_test>\<open>
   5.102 +fun atom_write_detail ctxt t = (writeln o (string_of_detail ctxt)) t;
   5.103 +fun atom_trace_detail ctxt t = (tracing o (string_of_detail ctxt)) t;
   5.104  \<close>
   5.105  
   5.106  (* contains the term a VAR(("*",_),_) ? *)
   5.107 @@ -365,16 +358,15 @@
   5.108    | var2free (Abs(s, T, t)) = Abs(s, T, var2free t)
   5.109    | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
   5.110    
   5.111 -(*isac_test*)
   5.112 +
   5.113 +\<^isac_test>\<open> (*TODO: check with new numerals --vv*)
   5.114  (* Logic.varify does NOT take care of 'Free ("1", _)'*)
   5.115 -fun free2var (t as Const _) = t
   5.116 -  | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
   5.117 -  | free2var (t as Var _) = t
   5.118 -  | free2var (t as Bound _) = t 
   5.119 -  | free2var (Abs (s, T, t)) = Abs (s, T, free2var t)
   5.120 -  | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
   5.121 -
   5.122 -\<^isac_test>\<open>
   5.123 +fun mk_Var (t as Const _) = t
   5.124 +  | mk_Var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
   5.125 +  | mk_Var (t as Var _) = t
   5.126 +  | mk_Var (t as Bound _) = t 
   5.127 +  | mk_Var (Abs (s, T, t)) = Abs (s, T, mk_Var t)
   5.128 +  | mk_Var (t1 $ t2) = (mk_Var t1) $ (mk_Var t2);
   5.129  \<close>
   5.130  
   5.131  fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]);

     6.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml	Wed Jan 11 09:23:18 2023 +0100
     6.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml	Wed Jan 11 11:38:01 2023 +0100
     6.3 @@ -3,7 +3,7 @@
     6.4     (c) due to copyright terms
     6.5  
     6.6  Probably this structure can be dropped due to improved reflection in Isabelle.
     6.7 -Here is a minimum of code required for theory Know_Store, 
     6.8 +Here is a minimum of code required for theory Know_Store,
     6.9  further code see structure ThmC.
    6.10  *)
    6.11  signature THEOREM_ISAC_DEF =

     7.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Wed Jan 11 09:23:18 2023 +0100
     7.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Wed Jan 11 11:38:01 2023 +0100
     7.3 @@ -330,7 +330,7 @@
     7.4  (*
     7.5  {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
     7.6  val (SOME ct) = parse thy ;
     7.7 -atomty thy (Thm.term_of ct);
     7.8 +TermC.atom_trace_detail @{context} (Thm.term_of ct);
     7.9  *)
    7.10  
    7.11  
    7.12 @@ -365,5 +365,5 @@
    7.13  (*
    7.14  {given=[],where_=[],find=[],with_=[],relate=[]}: string model;
    7.15  val (SOME ct) = parse thy ;
    7.16 -atomty thy (Thm.term_of ct);
    7.17 +TermC.atom_trace_detail @{context} (Thm.term_of ct);
    7.18  *)

     8.1 --- a/src/Tools/isac/Specify/Specify.thy	Wed Jan 11 09:23:18 2023 +0100
     8.2 +++ b/src/Tools/isac/Specify/Specify.thy	Wed Jan 11 11:38:01 2023 +0100
     8.3 @@ -24,7 +24,6 @@
     8.4  
     8.5  ML \<open>
     8.6  \<close> ML \<open>
     8.7 -ThyC.get_theory_PIDE
     8.8  \<close> ML \<open>
     8.9  \<close> ML \<open>
    8.10  \<close>

     9.1 --- a/src/Tools/isac/Specify/m-match.sml	Wed Jan 11 09:23:18 2023 +0100
     9.2 +++ b/src/Tools/isac/Specify/m-match.sml	Wed Jan 11 11:38:01 2023 +0100
     9.3 @@ -153,6 +153,8 @@
     9.4     an type-error is reported immediately, raises an exn, 
     9.5     subsequent handling of exn provides 2nd part of error message *)
     9.6  fun mtc thy (str, (dsc, _)) (ty $ var) =
     9.7 +    let val ctxt = Proof_Context.init_global thy
     9.8 +    in
     9.9      ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
    9.10        SOME (([1], str, dsc, (*[var]*)
    9.11  	    Input_Descript.split' (dsc, var))) (*:ori without leading #*))
    9.12 @@ -160,16 +162,19 @@
    9.13  	      (tracing (dashs 70 ^ "\n"
    9.14  	        ^ "*** ERROR while creating the items for the model of the ->problem\n"
    9.15  	        ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
    9.16 -	        ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
    9.17 -	        ^ "*** description: " ^ TermC.term_detail2str dsc
    9.18 -	        ^ "*** value: " ^ TermC.term_detail2str var
    9.19 -	        ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
    9.20 +	        ^ "*** item (->description ->value): " ^ UnparseC.term_in_ctxt ctxt dsc ^ " " ^ UnparseC.term_in_ctxt ctxt var ^ "\n"
    9.21 +	        ^ "*** description: " ^ TermC.string_of_detail ctxt dsc
    9.22 +	        ^ "*** value: " ^ TermC.string_of_detail ctxt var
    9.23 +	        ^ "*** typeconstructor in script: " ^ TermC.string_of_detail ctxt ty
    9.24  	        ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
    9.25  	        ^ "*** " ^ dots 66);
    9.26            writeln (@{make_string} e);
    9.27            Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
    9.28        NONE))
    9.29 -  | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
    9.30 +    end
    9.31 +  | mtc thy _ t =
    9.32 +    let val ctxt = Proof_Context.init_global thy
    9.33 +    in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term_in_ctxt ctxt t) end
    9.34  
    9.35  (* match each pat of the model-pattern with an actual argument;
    9.36     precondition: copy-named vars are filtered out            *)

    10.1 --- a/test/Tools/isac/ADDTESTS/Test_Units.thy	Wed Jan 11 09:23:18 2023 +0100
    10.2 +++ b/test/Tools/isac/ADDTESTS/Test_Units.thy	Wed Jan 11 11:38:01 2023 +0100
    10.3 @@ -29,7 +29,7 @@
    10.4  
    10.5  ML \<open>
    10.6  Thm.prop_of @{thm SI1m__cm};
    10.7 -TermC.atomt (Thm.prop_of @{thm SI1m__cm});
    10.8 +TermC.atom_trace @{context} (Thm.prop_of @{thm SI1m__cm});
    10.9  \<close>
   10.10  
   10.11  (*--------------------- broken Isabelle2015->17 -------------

    11.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jan 11 09:23:18 2023 +0100
    11.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jan 11 11:38:01 2023 +0100
    11.3 @@ -338,7 +338,7 @@
    11.4  ML \<open>
    11.5    val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
    11.6    UnparseC.term solutions;
    11.7 -  atomty solutions;
    11.8 +  TermC.atom_trace_detail @{context} solutions;
    11.9  \<close>
   11.10  
   11.11  subsubsection \<open>Get Solutions out of a List\<close>
   11.12 @@ -622,7 +622,7 @@
   11.13    val SOME (t1,_) = 
   11.14      rewrite_ @{theory} e_rew_ord Rule_Set.empty false 
   11.15               @{thm ansatz_2nd_order} expr';
   11.16 -  UnparseC.term t1; atomty t1;
   11.17 +  UnparseC.term t1; TermC.atom_trace_detail @{context} t1;
   11.18    val eq1 = HOLogic.mk_eq (expr', t1);
   11.19    UnparseC.term eq1;
   11.20  \<close>
   11.21 @@ -1081,7 +1081,7 @@
   11.22  
   11.23    parse thy str;
   11.24    val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
   11.25 -  atomty sc;
   11.26 +  TermC.atom_trace_detail @{context} sc;
   11.27  \<close>
   11.28  
   11.29  text \<open>\noindent This ruleset contains all functions that are in the script; 
   11.30 @@ -1238,7 +1238,7 @@
   11.31      = (#program o MethodC.from_store ctxt) ["SignalProcessing",
   11.32                          "Z_Transform",
   11.33                          "Inverse"];
   11.34 -  atomty sc;
   11.35 +  TermC.atom_trace_detail @{context} sc;
   11.36  \<close>
   11.37  
   11.38  subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>

    12.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Wed Jan 11 09:23:18 2023 +0100
    12.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Wed Jan 11 11:38:01 2023 +0100
    12.3 @@ -767,7 +767,7 @@
    12.4  \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
    12.5  \ \ val\ SOME\ solutions\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    12.6  \ \ term{\isadigit{2}}str\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    12.7 -\ \ atomty\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    12.8 +\ \ TermC.atom_trace_detail @{context}\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    12.9  {\isaliteral{2A7D}{\isacharverbatimclose}}%
   12.10  \endisatagML
   12.11  {\isafoldML}%
   12.12 @@ -1162,7 +1162,7 @@
   12.13  thm\ ansatz{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}nd{\isaliteral{5F}{\isacharunderscore}}order{}%
   12.14  \endisaantiq
   12.15  \ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.16 -\ \ term{\isadigit{2}}str\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ atomty\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.17 +\ \ term{\isadigit{2}}str\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ TermC.atom_trace_detail @{context}\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.18  \ \ val\ eq{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{28}{\isacharparenleft}}expr{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.19  \ \ term{\isadigit{2}}str\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.20  {\isaliteral{2A7D}{\isacharverbatimclose}}%
   12.21 @@ -2057,7 +2057,7 @@
   12.22  \isanewline
   12.23  \ \ parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.24  \ \ val\ sc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}inst{\isaliteral{5F}{\isacharunderscore}}abs\ thy{\isaliteral{29}{\isacharparenright}}\ o\ term{\isaliteral{5F}{\isacharunderscore}}of\ o\ the\ o\ {\isaliteral{28}{\isacharparenleft}}parse\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.25 -\ \ atomty\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.26 +\ \ TermC.atom_trace_detail @{context}\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.27  {\isaliteral{2A7D}{\isacharverbatimclose}}%
   12.28  \endisatagML
   12.29  {\isafoldML}%
   12.30 @@ -2294,7 +2294,7 @@
   12.31  \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{23}{\isacharhash}}scr\ o\ get{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   12.32  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
   12.33  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.34 -\ \ atomty\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.35 +\ \ TermC.atom_trace_detail @{context}\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   12.36  {\isaliteral{2A7D}{\isacharverbatimclose}}%
   12.37  \endisatagML
   12.38  {\isafoldML}%

    13.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Wed Jan 11 09:23:18 2023 +0100
    13.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Wed Jan 11 11:38:01 2023 +0100
    13.3 @@ -80,7 +80,7 @@
    13.4  \<close>
    13.5  ML \<open>
    13.6    val t = @{term "a + b * 9"};
    13.7 -  TermC.atomwy t;
    13.8 +  TermC.atom_write_detail @{context} t;
    13.9  \<close>
   13.10  text \<open>Please, observe that in this case (whenever 'writeln' is involved, even 
   13.11    invisibly) the output of 'atomwy t' is placed on top of the 'Output' window.

    14.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Wed Jan 11 09:23:18 2023 +0100
    14.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Wed Jan 11 11:38:01 2023 +0100
    14.3 @@ -68,7 +68,8 @@
    14.4    http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html
    14.5  \<close>
    14.6  ML \<open>
    14.7 -val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; UnparseC.term t;
    14.8 +val t = @{term "%x. x^2 + x + y"};
    14.9 +TermC.atom_write_detail @{context} t; UnparseC.term_in_ctxt @{context} t;
   14.10  \<close>
   14.11  text \<open>Since this notation does not conform to present high-school matheatics
   14.12    ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation

    15.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 09:23:18 2023 +0100
    15.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 11:38:01 2023 +0100
    15.3 @@ -232,7 +232,7 @@
    15.4  "----------- Pattern.match ------------------------------";
    15.5  "----------- Pattern.match ------------------------------";
    15.6   val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";
    15.7 - val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
    15.8 + val pat = (TermC.mk_Var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
    15.9   (*        ! \<up>  \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)
   15.10   val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
   15.11  (*default_print_depth 3; 999*) insts; 
   15.12 @@ -267,7 +267,7 @@
   15.13  
   15.14  "----- test 1: OK";
   15.15   val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
   15.16 - tracing "paIsa=..."; TermC.atomty pa; tracing "...=paIsa";
   15.17 + tracing "paIsa=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paIsa";
   15.18  (*** 
   15.19  *** Const (op =, real => real => bool)
   15.20  *** . Var ((a, 0), real)
   15.21 @@ -284,7 +284,7 @@
   15.22  
   15.23  "----- test 2: Nok";
   15.24   val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
   15.25 - tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2";
   15.26 + tracing "paLo2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paLo2";
   15.27  (*** 
   15.28  *** Const (op =, real => real => bool)
   15.29  *** . Var ((a, 0), real)
   15.30 @@ -303,8 +303,8 @@
   15.31    else ();*)
   15.32  
   15.33  "----- test 3: OK";
   15.34 - val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
   15.35 - tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2";
   15.36 + val pa = TermC.mk_Var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
   15.37 + tracing "paF2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paF2";
   15.38  (*** 
   15.39  *** Const (op =, real => real => bool)
   15.40  *** . Var ((a, 0), real)
   15.41 @@ -320,7 +320,7 @@
   15.42     else ();
   15.43  
   15.44  "----- test 4=3 with specific data";
   15.45 - val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0");
   15.46 + val pa = TermC.mk_Var (TermC.parse_test @{context} "M_b 0");
   15.47  "----- test 4a true";
   15.48   val tm = TermC.parse_test @{context} "M_b 0";
   15.49   if TermC.matches thy tm pa then () 
   15.50 @@ -335,14 +335,14 @@
   15.51  "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";
   15.52  (* added after Isabelle2015->17
   15.53  > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; 
   15.54 -> TermC.atomty (Thm.term_of ct);
   15.55 +> TermC.atom_trace_detail @{context} (Thm.term_of ct);
   15.56  *** -------------
   15.57  *** Const ( Nat.op ^, ['a, nat] => 'a)
   15.58  ***   Const ( uminus, 'a => 'a)
   15.59  ***     Free ( #5, 'a)
   15.60  ***   Free ( #3, nat)                
   15.61  > val (SOME ct) = TermC.parse thy "R=R"; 
   15.62 -> TermC.atomty (Thm.term_of ct);
   15.63 +> TermC.atom_trace_detail @{context} (Thm.term_of ct);
   15.64  *** -------------
   15.65  *** Const ( op =, [real, real] => bool)
   15.66  ***   Free ( R, real)

    16.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml	Wed Jan 11 09:23:18 2023 +0100
    16.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml	Wed Jan 11 11:38:01 2023 +0100
    16.3 @@ -56,10 +56,10 @@
    16.4        Const ("processed_by_Isabelle_Isac", _) = ttt;
    16.5  
    16.6  (* check the type structure *)
    16.7 -atomtyp T3;
    16.8 +TermC.atom_typ @{context} T3;
    16.9  Type (\<^type_name>\<open>real\<close>, []);
   16.10  
   16.11 -atomtyp T2;
   16.12 +TermC.atom_typ @{context} T2;
   16.13  (*
   16.14  *** Type (fun,[
   16.15  *** . Type (Real.real,[])
   16.16 @@ -75,7 +75,7 @@
   16.17      Type (\<^type_name>\<open>real\<close>, []), 
   16.18      Type (\<^type_name>\<open>real\<close>, [])])]);
   16.19  
   16.20 -atomtyp T1;
   16.21 +TermC.atom_typ @{context} T1;
   16.22  (*
   16.23  *** Type (fun,[
   16.24  *** . Type (Real.real,[])

    17.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Wed Jan 11 09:23:18 2023 +0100
    17.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Wed Jan 11 11:38:01 2023 +0100
    17.3 @@ -646,7 +646,7 @@
    17.4  case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => ()
    17.5  	| _ => raise 
    17.6  	      error "diff.sml behav.changed for CAS Diff (..., x)";
    17.7 -TermC.atomty t;
    17.8 +TermC.atom_trace_detail @{context} t;
    17.9  "-----------------------------------------------------------------";
   17.10  (*1>*)States.reset ();
   17.11  (*2>*)CalcTree @{context} [([], References.empty)];

    18.1 --- a/test/Tools/isac/Knowledge/algein.sml	Wed Jan 11 09:23:18 2023 +0100
    18.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Wed Jan 11 11:38:01 2023 +0100
    18.3 @@ -27,8 +27,8 @@
    18.4  \ in t_t)"
    18.5  ;
    18.6  val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
    18.7 -TermC.atomty sc;
    18.8 -atomt sc;
    18.9 +TermC.atom_trace_detail @{context} sc;
   18.10 +TermC.atom_trace @{context} sc;
   18.11  
   18.12  "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
   18.13  "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    19.1 --- a/test/Tools/isac/Knowledge/diff.sml	Wed Jan 11 09:23:18 2023 +0100
    19.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Wed Jan 11 11:38:01 2023 +0100
    19.3 @@ -223,16 +223,16 @@
    19.4  val v_ = TermC.parse_test @{context} "v_v";
    19.5  val v  = TermC.parse_test @{context} "s";
    19.6  val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
    19.7 -TermC.atomty screxp0;
    19.8 +TermC.atom_trace_detail @{context} screxp0;
    19.9  
   19.10  val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
   19.11  UnparseC.term screxp1;
   19.12 -TermC.atomty screxp1;
   19.13 +TermC.atom_trace_detail @{context} screxp1;
   19.14  
   19.15  val SOME (f'_,_) = rewrite_set_ ctxt false srls_diff screxp1; 
   19.16  if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then ()
   19.17  else error "diff.sml: diff.behav. in 'primed'";
   19.18 -TermC.atomty f'_;
   19.19 +TermC.atom_trace_detail @{context} f'_;
   19.20  
   19.21  val str = "Program DiffEqScr (f_f::bool) (v_v::real) =                         \
   19.22  \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))           \

    20.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Jan 11 09:23:18 2023 +0100
    20.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Jan 11 11:38:01 2023 +0100
    20.3 @@ -81,7 +81,7 @@
    20.4  "----------- problems --------------------------------------------";
    20.5  "----------- problems --------------------------------------------";
    20.6  val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";
    20.7 -TermC.atomty t;
    20.8 +TermC.atom_trace_detail @{context} t;
    20.9  val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 
   20.10  			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
   20.11  			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
   20.12 @@ -93,13 +93,13 @@
   20.13  else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
   20.14  
   20.15  val SOME t = TermC.parseNEW ctxt "solution LL";
   20.16 -TermC.atomty t;
   20.17 +TermC.atom_trace_detail @{context} t;
   20.18  val SOME t = TermC.parseNEW ctxt "solution LL";
   20.19 -TermC.atomty t;
   20.20 +TermC.atom_trace_detail @{context} t;
   20.21  
   20.22  val t = TermC.parse_test @{context} 
   20.23  "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
   20.24 -TermC.atomty t;
   20.25 +TermC.atom_trace_detail @{context} t;
   20.26  val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
   20.27    "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
   20.28  (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
   20.29 @@ -502,7 +502,7 @@
   20.30  val es_ = Free ("es_", "bool List.list") : Term.term
   20.31  
   20.32  > val pre1 = hd pres;
   20.33 -TermC.atomty pre1;
   20.34 +TermC.atom_trace_detail @{context} pre1;
   20.35  ***
   20.36  *** Const (op =, [real, real] => bool)
   20.37  *** . Const (ListG.length_, real list => real)

    21.1 --- a/test/Tools/isac/Knowledge/logexp.sml	Wed Jan 11 09:23:18 2023 +0100
    21.2 +++ b/test/Tools/isac/Knowledge/logexp.sml	Wed Jan 11 11:38:01 2023 +0100
    21.3 @@ -32,7 +32,7 @@
    21.4  val t = TermC.parse_test @{context} "(2 log x)";
    21.5  val t = TermC.parse_test @{context} "(2 log x) = 3";
    21.6  val t = TermC.parse_test @{context} "matches ((?a log x) = ?b) ((2 log x) = 3)";
    21.7 -TermC.atomty t;
    21.8 +TermC.atom_trace_detail @{context} t;
    21.9  
   21.10  
   21.11  val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"];

    22.1 --- a/test/Tools/isac/Knowledge/poly-2.sml	Wed Jan 11 09:23:18 2023 +0100
    22.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml	Wed Jan 11 11:38:01 2023 +0100
    22.3 @@ -172,7 +172,7 @@
    22.4  "-------- investigate (new 2002) uniary minus --------------------------------------------------";
    22.5  "-------- investigate (new 2002) uniary minus --------------------------------------------------";
    22.6  val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
    22.7 -TermC.atomty t;
    22.8 +TermC.atom_trace_detail @{context} t;
    22.9  (*
   22.10  *** Const (HOL.Trueprop, bool => prop)
   22.11  *** . Const (HOL.eq, real => real => bool)
   22.12 @@ -192,7 +192,7 @@
   22.13  
   22.14  
   22.15  val t = TermC.parseNEW' thy "- 1";
   22.16 -TermC.atomty t;
   22.17 +TermC.atom_trace_detail @{context} t;
   22.18  (*
   22.19  *** 
   22.20  *** Free (- 1, real)
   22.21 @@ -206,7 +206,7 @@
   22.22  (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
   22.23  (*----------------------------------- vvvvv -------------------------------------------*)
   22.24  val t = TermC.parseNEW' thy "-x";
   22.25 -TermC.atomty t;
   22.26 +TermC.atom_trace_detail @{context} t;
   22.27  (**** -------------
   22.28  *** Free ( -x, real)*)
   22.29  case t of
   22.30 @@ -214,7 +214,7 @@
   22.31  | _ => error "internal representation of \"-x\" changed";
   22.32  (*----------------------------------- vvvvv -------------------------------------------*)
   22.33  val t = TermC.parseNEW' thy "- x";
   22.34 -TermC.atomty t;
   22.35 +TermC.atom_trace_detail @{context} t;
   22.36  (**** -------------
   22.37  *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
   22.38  case t of
   22.39 @@ -222,7 +222,7 @@
   22.40  | _ => error "internal representation of \"- x\" changed";
   22.41  (*----------------------------------- vvvvvv ------------------------------------------*)
   22.42  val t = TermC.parseNEW' thy "-(x)";
   22.43 -TermC.atomty t;
   22.44 +TermC.atom_trace_detail @{context} t;
   22.45  (**** -------------
   22.46  *** Free ( -x, real)*)
   22.47  case t of

    23.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml	Wed Jan 11 09:23:18 2023 +0100
    23.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Wed Jan 11 11:38:01 2023 +0100
    23.3 @@ -284,16 +284,16 @@
    23.4  (* steps in rls d2_polyeq_bdv_only_simplify:*)
    23.5  
    23.6  (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
    23.7 -t |> UnparseC.term; t |> TermC.atomty;
    23.8 +t |> UnparseC.term; t |> TermC.atom_trace_detail @{context};
    23.9  val thm = @{thm d2_prescind1};
   23.10 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
   23.11 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atom_trace_detail @{context};
   23.12  val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';
   23.13  
   23.14  (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 
   23.15                                                                          --> x = 0 | -6 + 5 * x = 0*)
   23.16 -t' |> UnparseC.term; t' |> TermC.atomty;
   23.17 +t' |> UnparseC.term; t' |> TermC.atom_trace_detail @{context};
   23.18  val thm = @{thm d2_reduce_equation1};
   23.19 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
   23.20 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atom_trace_detail @{context};
   23.21  val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';
   23.22  (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
   23.23     instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"

    24.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Jan 11 09:23:18 2023 +0100
    24.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Jan 11 11:38:01 2023 +0100
    24.3 @@ -339,7 +339,7 @@
    24.4  \    (Try (Rewrite_Set fasse_zusammen False)) #>     \
    24.5  \    (Try (Rewrite_Set verschoenere False))) t_t)"
    24.6  val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
    24.7 -TermC.atomty sc;
    24.8 +TermC.atom_trace_detail @{context} sc;
    24.9  
   24.10  "----------- me simplification.for_polynomials.with_minus";
   24.11  "----------- me simplification.for_polynomials.with_minus";
   24.12 @@ -446,7 +446,7 @@
   24.13  \            (Try (Repeat (Calculate ''PLUS''))) #>  \
   24.14  \            (Try (Repeat (Calculate ''MINUS''))))) e_e)"
   24.15  val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
   24.16 -TermC.atomty sc;
   24.17 +TermC.atom_trace_detail @{context} sc;
   24.18  
   24.19  "----------- pbl polynom probe -----------------------------------";
   24.20  "----------- pbl polynom probe -----------------------------------";

    25.1 --- a/test/Tools/isac/Knowledge/wn.sml	Wed Jan 11 09:23:18 2023 +0100
    25.2 +++ b/test/Tools/isac/Knowledge/wn.sml	Wed Jan 11 11:38:01 2023 +0100
    25.3 @@ -5,7 +5,7 @@
    25.4  
    25.5  
    25.6   val t = TermC.parse_test @{context} "solve (a*x + b = c, x)";
    25.7 - TermC.atomty t;
    25.8 + TermC.atom_trace_detail @{context} t;
    25.9  (*
   25.10  "\n*** -------------"
   25.11  "\n*** Const ( Equation.solve, bool * real => bool list)"

    26.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Jan 11 09:23:18 2023 +0100
    26.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Jan 11 11:38:01 2023 +0100
    26.3 @@ -476,7 +476,7 @@
    26.4  "----------- 2011 thms with axclasses ----------------------------------------------------------";
    26.5  val thm = @{thm div_by_1};
    26.6  val prop = Thm.prop_of thm;
    26.7 -TermC.atomty prop;                                     (*Type 'a*)
    26.8 +TermC.atom_trace_detail @{context} prop;                                     (*Type 'a*)
    26.9  val t = TermC.parse_test @{context} "(2*x)/1";                      (*Type real*)
   26.10  
   26.11  val (thy, ro, er, inst) = 

    27.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Jan 11 09:23:18 2023 +0100
    27.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Jan 11 11:38:01 2023 +0100
    27.3 @@ -199,8 +199,8 @@
    27.4  " _________________ rewrite x=4_________________ ";
    27.5  (*
    27.6  rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
    27.7 -TermC.atomty (Thm.prop_of (!tthm));
    27.8 -TermC.atomty (Thm.term_of (!tct));
    27.9 +TermC.atom_trace_detail @{context} (Thm.prop_of (!tthm));
   27.10 +TermC.atom_trace_detail @{context} (Thm.term_of (!tct));
   27.11  *)
   27.12  val thy' = "Test";
   27.13  val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
   27.14 @@ -375,7 +375,7 @@
   27.15  
   27.16  (*
   27.17  val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
   27.18 -TermC.atomty t;
   27.19 +TermC.atom_trace_detail @{context} t;
   27.20  *)
   27.21  
   27.22  

    28.1 --- a/test/Tools/isac/OLDTESTS/script.sml	Wed Jan 11 09:23:18 2023 +0100
    28.2 +++ b/test/Tools/isac/OLDTESTS/script.sml	Wed Jan 11 11:38:01 2023 +0100
    28.3 @@ -252,7 +252,7 @@
    28.4     \  (Try (Repeat (Rewrite square_equation_left))) #> \
    28.5     \  (Try (Repeat (Rewrite radd_0)))))\
    28.6     \ e_e            ");
    28.7 -TermC.atomty sc;
    28.8 +TermC.atom_trace_detail @{context} sc;
    28.9  val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"],
   28.10  		     ["Test", "sqrt-equ-test"]);
   28.11  val c = []; 

    29.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Wed Jan 11 09:23:18 2023 +0100
    29.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Wed Jan 11 11:38:01 2023 +0100
    29.3 @@ -36,10 +36,10 @@
    29.4  
    29.5  val t = (Thm.term_of o the o (TermC.parse Test.thy)) 
    29.6  	    "is_rootequation_in (sqrt(x)=1) x";
    29.7 -TermC.atomty t;
    29.8 +TermC.atom_trace_detail @{context} t;
    29.9  val t = (Thm.term_of o the o (TermC.parse (theory "Isac_Knowledge"))) 
   29.10  	    "is_rootequation_in (sqrt(x)=1) x";
   29.11 -TermC.atomty t;
   29.12 +TermC.atom_trace_detail @{context} t;
   29.13  
   29.14  (*
   29.15  val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;

    30.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml	Wed Jan 11 09:23:18 2023 +0100
    30.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml	Wed Jan 11 11:38:01 2023 +0100
    30.3 @@ -152,7 +152,7 @@
    30.4  val auto_script = 
    30.5    Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational");
    30.6  writeln(UnparseC.term auto_script);
    30.7 -TermC.atomty auto_script;
    30.8 +TermC.atom_trace_detail @{context} auto_script;
    30.9  (*** 
   30.10  *** Const (Program.Stepwise, 'z => 'z => 'z)
   30.11  *** . Free (t_t, 'z)

    31.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Jan 11 09:23:18 2023 +0100
    31.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Jan 11 11:38:01 2023 +0100
    31.3 @@ -141,7 +141,7 @@
    31.4  
    31.5  (*--------------(3): is_num works ?: -------------------------------------*)
    31.6   val t = TermC.parseNEW' ctxt "2 is_num";
    31.7 - TermC.atomty t;
    31.8 + TermC.atom_trace_detail @{context} t;
    31.9   rewrite_set_ ctxt false tval_rls t;
   31.10  (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
   31.11  

    32.1 --- a/test/Tools/isac/ProgLang/listC.sml	Wed Jan 11 09:23:18 2023 +0100
    32.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Wed Jan 11 11:38:01 2023 +0100
    32.3 @@ -48,9 +48,9 @@
    32.4  val prog_expr = get_rls @{context} "prog_expr"
    32.5  
    32.6  val t = TermC.parse_test @{context} "NTH 1 [a,b,c,d,e]";
    32.7 -TermC.atomty t;
    32.8 +TermC.atom_trace_detail @{context} t;
    32.9  val thm = Thm.prop_of @{thm NTH_NIL};
   32.10 -TermC.atomty thm;
   32.11 +TermC.atom_trace_detail @{context} thm;
   32.12  val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
   32.13  if UnparseC.term t' = "a" then () 
   32.14  else error "NTH 1 [a,b,c,d,e] = a ..changed";
   32.15 @@ -65,14 +65,14 @@
   32.16               (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
   32.17  | _ => error "ListC.NTH changed";
   32.18  val thm = Thm.prop_of @{thm NTH_CONS};
   32.19 -TermC.atomty thm;
   32.20 +TermC.atom_trace_detail @{context} thm;
   32.21  val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false  @{thm NTH_CONS} t;
   32.22  if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
   32.23  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
   32.24  
   32.25  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
   32.26  val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
   32.27 -TermC.atomty t;
   32.28 +TermC.atom_trace_detail @{context} t;
   32.29  
   32.30  val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
   32.31  if UnparseC.term t' = "c" then () 

    33.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml	Wed Jan 11 09:23:18 2023 +0100
    33.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml	Wed Jan 11 11:38:01 2023 +0100
    33.3 @@ -346,7 +346,7 @@
    33.4  "---------fun eval_sameFunId -------------------------------------------------------------------";
    33.5  "---------fun eval_sameFunId -------------------------------------------------------------------";
    33.6  "---------fun eval_sameFunId -------------------------------------------------------------------";
    33.7 -val t = @{term "M_b L"}; TermC.atomty t;
    33.8 +val t = @{term "M_b L"}; TermC.atom_trace_detail @{context} t;
    33.9  val t as f1 $ _ = @{term "M_b L"};
   33.10  val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
   33.11  f1 = f2 (*true*);

    34.1 --- a/test/Tools/isac/Specify/input-descript.sml	Wed Jan 11 09:23:18 2023 +0100
    34.2 +++ b/test/Tools/isac/Specify/input-descript.sml	Wed Jan 11 11:38:01 2023 +0100
    34.3 @@ -18,7 +18,7 @@
    34.4  val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>, 
    34.5    Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]), 
    34.6      Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"};
    34.7 -atomtyp (type_of t);
    34.8 +TermC.atom_typ @{context} (type_of t);
    34.9  if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed";
   34.10  "----- fun Input_Descript.for_real -----";
   34.11  if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed";

    35.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Jan 11 09:23:18 2023 +0100
    35.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Jan 11 11:38:01 2023 +0100
    35.3 @@ -124,7 +124,7 @@
    35.4    open P_Model;                (* NONE *)
    35.5    open Rewrite;
    35.6    open Eval;                   get_pair;
    35.7 -  open TermC;                  atomt;
    35.8 +  open TermC;
    35.9    open Rule;
   35.10    open Rule_Set;               Sequence;
   35.11    open Eval_Def

    36.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Wed Jan 11 09:23:18 2023 +0100
    36.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed Jan 11 11:38:01 2023 +0100
    36.3 @@ -124,7 +124,7 @@
    36.4    open P_Model;                (* NONE *)
    36.5    open Rewrite;
    36.6    open Eval;                   get_pair;
    36.7 -  open TermC;                  atomt;
    36.8 +  open TermC;
    36.9    open Rule;
   36.10    open Rule_Set;               Sequence;
   36.11    open Eval_Def