1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4  ML \<open>
     1.5    val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
     1.6    UnparseC.term solutions;
     1.7 -  atomty solutions;
     1.8 +  TermC.atom_trace_detail @{context} solutions;
     1.9  \<close>
    1.10  
    1.11  subsubsection \<open>Get Solutions out of a List\<close>
    1.12 @@ -622,7 +622,7 @@
    1.13    val SOME (t1,_) = 
    1.14      rewrite_ @{theory} e_rew_ord Rule_Set.empty false 
    1.15               @{thm ansatz_2nd_order} expr';
    1.16 -  UnparseC.term t1; atomty t1;
    1.17 +  UnparseC.term t1; TermC.atom_trace_detail @{context} t1;
    1.18    val eq1 = HOLogic.mk_eq (expr', t1);
    1.19    UnparseC.term eq1;
    1.20  \<close>
    1.21 @@ -1081,7 +1081,7 @@
    1.22  
    1.23    parse thy str;
    1.24    val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.25 -  atomty sc;
    1.26 +  TermC.atom_trace_detail @{context} sc;
    1.27  \<close>
    1.28  
    1.29  text \<open>\noindent This ruleset contains all functions that are in the script; 
    1.30 @@ -1238,7 +1238,7 @@
    1.31      = (#program o MethodC.from_store ctxt) ["SignalProcessing",
    1.32                          "Z_Transform",
    1.33                          "Inverse"];
    1.34 -  atomty sc;
    1.35 +  TermC.atom_trace_detail @{context} sc;
    1.36  \<close>
    1.37  
    1.38  subsubsection \<open>Stepwise Check the Program\label{sec:stepcheck}\<close>