diff -r b2ff1902420f -r 06ec8abfd3bc test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
--- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jan 11 09:23:18 2023 +0100
+++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jan 11 11:38:01 2023 +0100
@@ -338,7 +338,7 @@
 ML \<open>
   val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
   UnparseC.term solutions;
-  atomty solutions;
+  TermC.atom_trace_detail @{context} solutions;
 \<close>
 
 subsubsection \<open>Get Solutions out of a List\<close>
@@ -622,7 +622,7 @@
   val SOME (t1,_) = 
     rewrite_ @{theory} e_rew_ord Rule_Set.empty false 
              @{thm ansatz_2nd_order} expr';
-  UnparseC.term t1; atomty t1;
+  UnparseC.term t1; TermC.atom_trace_detail @{context} t1;
   val eq1 = HOLogic.mk_eq (expr', t1);
   UnparseC.term eq1;
 \<close>
@@ -1081,7 +1081,7 @@
 
   parse thy str;
   val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
-  atomty sc;
+  TermC.atom_trace_detail @{context} sc;
 \<close>
 
 text \<open>\noindent This ruleset contains all functions that are in the script; 
@@ -1238,7 +1238,7 @@
     = (#program o MethodC.from_store ctxt) ["SignalProcessing",
                         "Z_Transform",
                         "Inverse"];
-  atomty sc;
+  TermC.atom_trace_detail @{context} sc;
 \<close>
 
 subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>