diff -r b2ff1902420f -r 06ec8abfd3bc test/Tools/isac/Knowledge/diff.sml
--- a/test/Tools/isac/Knowledge/diff.sml	Wed Jan 11 09:23:18 2023 +0100
+++ b/test/Tools/isac/Knowledge/diff.sml	Wed Jan 11 11:38:01 2023 +0100
@@ -223,16 +223,16 @@
 val v_ = TermC.parse_test @{context} "v_v";
 val v  = TermC.parse_test @{context} "s";
 val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
-TermC.atomty screxp0;
+TermC.atom_trace_detail @{context} screxp0;
 
 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
 UnparseC.term screxp1;
-TermC.atomty screxp1;
+TermC.atom_trace_detail @{context} screxp1;
 
 val SOME (f'_,_) = rewrite_set_ ctxt false srls_diff screxp1; 
 if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then ()
 else error "diff.sml: diff.behav. in 'primed'";
-TermC.atomty f'_;
+TermC.atom_trace_detail @{context} f'_;
 
 val str = "Program DiffEqScr (f_f::bool) (v_v::real) =                         \
 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))           \