equal
deleted
inserted
replaced
102 \<close> |
102 \<close> |
103 |
103 |
104 ML \<open> |
104 ML \<open> |
105 "artifically inject assumptions"; |
105 "artifically inject assumptions"; |
106 val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p); |
106 val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p); |
107 val ctxt = Stool.insert_assumptions [TermC.str2term "x < sub_asm_out", |
107 val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out", |
108 TermC.str2term "a < sub_asm_local"] cres; |
108 TermC.str2term "a < sub_asm_local"] cres; |
109 val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt)); |
109 val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt)); |
110 \<close> |
110 \<close> |
111 |
111 |
112 ML \<open> |
112 ML \<open> |