1.1 --- a/test/Tools/isac/Knowledge/poly-2.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -172,7 +172,7 @@
     1.4  "-------- investigate (new 2002) uniary minus --------------------------------------------------";
     1.5  "-------- investigate (new 2002) uniary minus --------------------------------------------------";
     1.6  val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
     1.7 -TermC.atomty t;
     1.8 +TermC.atom_trace_detail @{context} t;
     1.9  (*
    1.10  *** Const (HOL.Trueprop, bool => prop)
    1.11  *** . Const (HOL.eq, real => real => bool)
    1.12 @@ -192,7 +192,7 @@
    1.13  
    1.14  
    1.15  val t = TermC.parseNEW' thy "- 1";
    1.16 -TermC.atomty t;
    1.17 +TermC.atom_trace_detail @{context} t;
    1.18  (*
    1.19  *** 
    1.20  *** Free (- 1, real)
    1.21 @@ -206,7 +206,7 @@
    1.22  (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
    1.23  (*----------------------------------- vvvvv -------------------------------------------*)
    1.24  val t = TermC.parseNEW' thy "-x";
    1.25 -TermC.atomty t;
    1.26 +TermC.atom_trace_detail @{context} t;
    1.27  (**** -------------
    1.28  *** Free ( -x, real)*)
    1.29  case t of
    1.30 @@ -214,7 +214,7 @@
    1.31  | _ => error "internal representation of \"-x\" changed";
    1.32  (*----------------------------------- vvvvv -------------------------------------------*)
    1.33  val t = TermC.parseNEW' thy "- x";
    1.34 -TermC.atomty t;
    1.35 +TermC.atom_trace_detail @{context} t;
    1.36  (**** -------------
    1.37  *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
    1.38  case t of
    1.39 @@ -222,7 +222,7 @@
    1.40  | _ => error "internal representation of \"- x\" changed";
    1.41  (*----------------------------------- vvvvvv ------------------------------------------*)
    1.42  val t = TermC.parseNEW' thy "-(x)";
    1.43 -TermC.atomty t;
    1.44 +TermC.atom_trace_detail @{context} t;
    1.45  (**** -------------
    1.46  *** Free ( -x, real)*)
    1.47  case t of