1.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -116,8 +116,8 @@
     1.4  ML \<open>
     1.5    "artifically inject assumptions";
     1.6    val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);
     1.7 -  val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out",
     1.8 -                                 TermC.str2term "a < sub_asm_local"] cres;
     1.9 +  val ctxt = ContextC.insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out",
    1.10 +                                 TermC.parse_test @{context} "a < sub_asm_local"] cres;
    1.11    val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
    1.12  \<close>
    1.13