diff -r b2ff1902420f -r 06ec8abfd3bc test/Tools/isac/Knowledge/poly-2.sml
--- a/test/Tools/isac/Knowledge/poly-2.sml	Wed Jan 11 09:23:18 2023 +0100
+++ b/test/Tools/isac/Knowledge/poly-2.sml	Wed Jan 11 11:38:01 2023 +0100
@@ -172,7 +172,7 @@
 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
-TermC.atomty t;
+TermC.atom_trace_detail @{context} t;
 (*
 *** Const (HOL.Trueprop, bool => prop)
 *** . Const (HOL.eq, real => real => bool)
@@ -192,7 +192,7 @@
 
 
 val t = TermC.parseNEW' thy "- 1";
-TermC.atomty t;
+TermC.atom_trace_detail @{context} t;
 (*
 *** 
 *** Free (- 1, real)
@@ -206,7 +206,7 @@
 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
 (*----------------------------------- vvvvv -------------------------------------------*)
 val t = TermC.parseNEW' thy "-x";
-TermC.atomty t;
+TermC.atom_trace_detail @{context} t;
 (**** -------------
 *** Free ( -x, real)*)
 case t of
@@ -214,7 +214,7 @@
 | _ => error "internal representation of \"-x\" changed";
 (*----------------------------------- vvvvv -------------------------------------------*)
 val t = TermC.parseNEW' thy "- x";
-TermC.atomty t;
+TermC.atom_trace_detail @{context} t;
 (**** -------------
 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
 case t of
@@ -222,7 +222,7 @@
 | _ => error "internal representation of \"- x\" changed";
 (*----------------------------------- vvvvvv ------------------------------------------*)
 val t = TermC.parseNEW' thy "-(x)";
-TermC.atomty t;
+TermC.atom_trace_detail @{context} t;
 (**** -------------
 *** Free ( -x, real)*)
 case t of