1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Jan 26 19:02:41 2023 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jan 28 13:21:39 2023 +0100
     1.3 @@ -133,10 +133,10 @@
     1.4    val ctxt = Proof_Context.init_global @{theory};
     1.5  (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
     1.6  
     1.7 -  val SOME fun1 = 
     1.8 -    TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term fun1;
     1.9 -  val SOME fun1' = 
    1.10 -    TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term fun1';
    1.11 +  val fun1 = 
    1.12 +    TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term_in_ctxt ctxt fun1;
    1.13 +  val fun1' = 
    1.14 +    TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term_in_ctxt ctxt fun1';
    1.15  \<close>
    1.16  
    1.17  subsubsection \<open>Prepare Numerator and Denominator\<close>
    1.18 @@ -262,7 +262,7 @@
    1.19         for this equation type. Later on {\sisac} should determine the type
    1.20         of the given equation self.\<close>
    1.21  ML \<open>
    1.22 -  val denominator = TermC.parseNEW ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
    1.23 +  val denominator = TermC.parse ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
    1.24    val fmz = ["equality (z \<up> 2 - 1/4*z - 1/8 = (0::real))",
    1.25               "solveFor z",
    1.26               "solutions L"];