doc-isac/mlehnfeld/bacc/projektbericht.tex
changeset 60566 04f8699d2c9d
parent 55467 2e9db65faf65
child 60658 1c089105f581
     1.1 --- a/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 07:44:22 2022 +0200
     1.2 +++ b/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 09:01:29 2022 +0200
     1.3 @@ -461,8 +461,8 @@
     1.4  ML {*
     1.5    "artifically inject assumptions";
     1.6    val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
     1.7 -  val ctxt = insert_assumptions [str2term "x < sub_asm_out",
     1.8 -                                 str2term "a < sub_asm_local"] cres;
     1.9 +  val ctxt = 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 = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
    1.12  *}
    1.13