1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  "----------- fun calculate_ --------------------------------------------------------------------";
     1.5  "----------- fun calculate_ --------------------------------------------------------------------";
     1.6  (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
     1.7 -val t = TermC.str2term "((1+2)*4/3) \<up> 2";
     1.8 +val t = TermC.parse_test @{context} "((1+2)*4/3) \<up> 2";
     1.9  val thy = @{theory};
    1.10  val ctxt = Proof_Context.init_global @{theory}
    1.11  val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun;
    1.12 @@ -145,7 +145,7 @@
    1.13   rewrite_set_ ctxt false tval_rls t;
    1.14  (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
    1.15  
    1.16 - val t = TermC.str2term "2 * x is_num";
    1.17 + val t = TermC.parse_test @{context} "2 * x is_num";
    1.18   val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"});
    1.19   
    1.20  
    1.21 @@ -320,7 +320,7 @@
    1.22  val (thy, op_, ef, arg) =
    1.23      (thy, "EqSystem.occur_exactly_in", 
    1.24       get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd,
    1.25 -     TermC.str2term
    1.26 +     TermC.parse_test @{context}
    1.27        "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
    1.28        );
    1.29  val SOME (str, simpl) = get_pair ctxt op_ ef arg;
    1.30 @@ -332,7 +332,7 @@
    1.31  "----------- calculate (2 * x is_num) -------------------";
    1.32  "----------- calculate (2 * x is_num) -------------------";
    1.33  "----------- calculate (2 * x is_num) -------------------";
    1.34 -val t = TermC.str2term "(2::real) * x is_num";
    1.35 +val t = TermC.parse_test @{context} "(2::real) * x is_num";
    1.36  
    1.37  val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test};
    1.38  if UnparseC.term t' = "(2 * x is_num) = False" then ()
    1.39 @@ -471,7 +471,7 @@
    1.40  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.41  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.42  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.43 -val t = TermC.str2term "sqrt 4";
    1.44 +val t = TermC.parse_test @{context} "sqrt 4";
    1.45  Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
    1.46  
    1.47  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =