1.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -232,7 +232,7 @@
     1.4  "----------- Pattern.match ------------------------------";
     1.5  "----------- Pattern.match ------------------------------";
     1.6   val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";
     1.7 - val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
     1.8 + val pat = (TermC.mk_Var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
     1.9   (*        ! \<up>  \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)
    1.10   val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
    1.11  (*default_print_depth 3; 999*) insts; 
    1.12 @@ -267,7 +267,7 @@
    1.13  
    1.14  "----- test 1: OK";
    1.15   val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
    1.16 - tracing "paIsa=..."; TermC.atomty pa; tracing "...=paIsa";
    1.17 + tracing "paIsa=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paIsa";
    1.18  (*** 
    1.19  *** Const (op =, real => real => bool)
    1.20  *** . Var ((a, 0), real)
    1.21 @@ -284,7 +284,7 @@
    1.22  
    1.23  "----- test 2: Nok";
    1.24   val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
    1.25 - tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2";
    1.26 + tracing "paLo2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paLo2";
    1.27  (*** 
    1.28  *** Const (op =, real => real => bool)
    1.29  *** . Var ((a, 0), real)
    1.30 @@ -303,8 +303,8 @@
    1.31    else ();*)
    1.32  
    1.33  "----- test 3: OK";
    1.34 - val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
    1.35 - tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2";
    1.36 + val pa = TermC.mk_Var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
    1.37 + tracing "paF2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paF2";
    1.38  (*** 
    1.39  *** Const (op =, real => real => bool)
    1.40  *** . Var ((a, 0), real)
    1.41 @@ -320,7 +320,7 @@
    1.42     else ();
    1.43  
    1.44  "----- test 4=3 with specific data";
    1.45 - val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0");
    1.46 + val pa = TermC.mk_Var (TermC.parse_test @{context} "M_b 0");
    1.47  "----- test 4a true";
    1.48   val tm = TermC.parse_test @{context} "M_b 0";
    1.49   if TermC.matches thy tm pa then () 
    1.50 @@ -335,14 +335,14 @@
    1.51  "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";
    1.52  (* added after Isabelle2015->17
    1.53  > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; 
    1.54 -> TermC.atomty (Thm.term_of ct);
    1.55 +> TermC.atom_trace_detail @{context} (Thm.term_of ct);
    1.56  *** -------------
    1.57  *** Const ( Nat.op ^, ['a, nat] => 'a)
    1.58  ***   Const ( uminus, 'a => 'a)
    1.59  ***     Free ( #5, 'a)
    1.60  ***   Free ( #3, nat)                
    1.61  > val (SOME ct) = TermC.parse thy "R=R"; 
    1.62 -> TermC.atomty (Thm.term_of ct);
    1.63 +> TermC.atom_trace_detail @{context} (Thm.term_of ct);
    1.64  *** -------------
    1.65  *** Const ( op =, [real, real] => bool)
    1.66  ***   Free ( R, real)