diff -r b2ff1902420f -r 06ec8abfd3bc test/Tools/isac/BaseDefinitions/termC.sml
--- a/test/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 09:23:18 2023 +0100
+++ b/test/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 11:38:01 2023 +0100
@@ -232,7 +232,7 @@
 "----------- Pattern.match ------------------------------";
 "----------- Pattern.match ------------------------------";
  val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";
- val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
+ val pat = (TermC.mk_Var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
  (*        ! \<up>  \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)
  val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
 (*default_print_depth 3; 999*) insts; 
@@ -267,7 +267,7 @@
 
 "----- test 1: OK";
  val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
- tracing "paIsa=..."; TermC.atomty pa; tracing "...=paIsa";
+ tracing "paIsa=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paIsa";
 (*** 
 *** Const (op =, real => real => bool)
 *** . Var ((a, 0), real)
@@ -284,7 +284,7 @@
 
 "----- test 2: Nok";
  val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
- tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2";
+ tracing "paLo2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paLo2";
 (*** 
 *** Const (op =, real => real => bool)
 *** . Var ((a, 0), real)
@@ -303,8 +303,8 @@
   else ();*)
 
 "----- test 3: OK";
- val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
- tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2";
+ val pa = TermC.mk_Var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
+ tracing "paF2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paF2";
 (*** 
 *** Const (op =, real => real => bool)
 *** . Var ((a, 0), real)
@@ -320,7 +320,7 @@
    else ();
 
 "----- test 4=3 with specific data";
- val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0");
+ val pa = TermC.mk_Var (TermC.parse_test @{context} "M_b 0");
 "----- test 4a true";
  val tm = TermC.parse_test @{context} "M_b 0";
  if TermC.matches thy tm pa then () 
@@ -335,14 +335,14 @@
 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";
 (* added after Isabelle2015->17
 > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; 
-> TermC.atomty (Thm.term_of ct);
+> TermC.atom_trace_detail @{context} (Thm.term_of ct);
 *** -------------
 *** Const ( Nat.op ^, ['a, nat] => 'a)
 ***   Const ( uminus, 'a => 'a)
 ***     Free ( #5, 'a)
 ***   Free ( #3, nat)                
 > val (SOME ct) = TermC.parse thy "R=R"; 
-> TermC.atomty (Thm.term_of ct);
+> TermC.atom_trace_detail @{context} (Thm.term_of ct);
 *** -------------
 *** Const ( op =, [real, real] => bool)
 ***   Free ( R, real)