diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/mlehnfeld/bacc/projektbericht.tex
--- a/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 09:01:29 2022 +0200
@@ -461,8 +461,8 @@
 ML {*
   "artifically inject assumptions";
   val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
-  val ctxt = insert_assumptions [str2term "x < sub_asm_out",
-                                 str2term "a < sub_asm_local"] cres;
+  val ctxt = insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out",
+                                 TermC.parse_test @{context} "a < sub_asm_local"] cres;
   val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
 *}