1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -48,9 +48,9 @@
     1.4  val prog_expr = get_rls @{context} "prog_expr"
     1.5  
     1.6  val t = TermC.parse_test @{context} "NTH 1 [a,b,c,d,e]";
     1.7 -TermC.atomty t;
     1.8 +TermC.atom_trace_detail @{context} t;
     1.9  val thm = Thm.prop_of @{thm NTH_NIL};
    1.10 -TermC.atomty thm;
    1.11 +TermC.atom_trace_detail @{context} thm;
    1.12  val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
    1.13  if UnparseC.term t' = "a" then () 
    1.14  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.15 @@ -65,14 +65,14 @@
    1.16               (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
    1.17  | _ => error "ListC.NTH changed";
    1.18  val thm = Thm.prop_of @{thm NTH_CONS};
    1.19 -TermC.atomty thm;
    1.20 +TermC.atom_trace_detail @{context} thm;
    1.21  val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false  @{thm NTH_CONS} t;
    1.22  if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    1.23  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.24  
    1.25  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.26  val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
    1.27 -TermC.atomty t;
    1.28 +TermC.atom_trace_detail @{context} t;
    1.29  
    1.30  val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
    1.31  if UnparseC.term t' = "c" then ()