1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  "----------- problems --------------------------------------------";
     1.5  "----------- problems --------------------------------------------";
     1.6  val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";
     1.7 -TermC.atomty t;
     1.8 +TermC.atom_trace_detail @{context} t;
     1.9  val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 
    1.10  			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
    1.11  			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
    1.12 @@ -93,13 +93,13 @@
    1.13  else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
    1.14  
    1.15  val SOME t = TermC.parseNEW ctxt "solution LL";
    1.16 -TermC.atomty t;
    1.17 +TermC.atom_trace_detail @{context} t;
    1.18  val SOME t = TermC.parseNEW ctxt "solution LL";
    1.19 -TermC.atomty t;
    1.20 +TermC.atom_trace_detail @{context} t;
    1.21  
    1.22  val t = TermC.parse_test @{context} 
    1.23  "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
    1.24 -TermC.atomty t;
    1.25 +TermC.atom_trace_detail @{context} t;
    1.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 " ^
    1.27    "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
    1.28  (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
    1.29 @@ -502,7 +502,7 @@
    1.30  val es_ = Free ("es_", "bool List.list") : Term.term
    1.31  
    1.32  > val pre1 = hd pres;
    1.33 -TermC.atomty pre1;
    1.34 +TermC.atom_trace_detail @{context} pre1;
    1.35  ***
    1.36  *** Const (op =, [real, real] => bool)
    1.37  *** . Const (ListG.length_, real list => real)