1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4      ];
     1.5  
     1.6  \<close> ML \<open>
     1.7 -  val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real";
     1.8 +  val t = TermC.parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real";
     1.9  \<close> ML \<open>
    1.10    val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
    1.11  (*rewrite__set_ called with 'Erls' for '|| z || < 1'*)
    1.12 @@ -408,17 +408,17 @@
    1.13  probably keep these test in test/Tools/isac/...
    1.14  (*mk_prod TermC.empty [];*)
    1.15  
    1.16 -val prod = mk_prod TermC.empty [str2term "x + 123"]; 
    1.17 +val prod = mk_prod TermC.empty [parse_test @{context} "x + 123"]; 
    1.18  UnparseC.term prod = "x + 123";
    1.19  
    1.20 -val sol = str2term "[z = 1 / 2, z = -1 / 4]";
    1.21 +val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
    1.22  val sols = HOLogic.dest_list sol;
    1.23  val facs = map fac_from_sol sols;
    1.24  val prod = mk_prod TermC.empty facs; 
    1.25  UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
    1.26  
    1.27  val prod = 
    1.28 -  mk_prod TermC.empty [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; 
    1.29 +  mk_prod TermC.empty [parse_test @{context} "x + 1", parse_test @{context} "x + 2", parse_test @{context} "x + 3"]; 
    1.30  UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)";
    1.31  *} *)
    1.32  ML \<open>
    1.33 @@ -427,7 +427,7 @@
    1.34      in mk_prod TermC.empty (map fac_from_sol ts) end;
    1.35  \<close>
    1.36  (* ML {*
    1.37 -val sol = str2term "[z = 1 / 2, z = -1 / 4]";
    1.38 +val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]";
    1.39  val fs = factors_from_solution sol;
    1.40  UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
    1.41  *} *)