equal
deleted
inserted
replaced
56 *) |
56 *) |
57 fun check_for' (res, inf) subst (id, pat) rls = |
57 fun check_for' (res, inf) subst (id, pat) rls = |
58 let |
58 let |
59 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
59 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
60 val (res', _, _, rewritten) = |
60 val (res', _, _, rewritten) = |
61 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord |
61 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty |
62 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
62 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
63 in |
63 in |
64 if rewritten then |
64 if rewritten then |
65 let |
65 let |
66 val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of |
66 val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of |
98 returns thm required by "fun in_fillform *) |
98 returns thm required by "fun in_fillform *) |
99 fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) = |
99 fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) = |
100 let |
100 let |
101 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
101 val ctxt = Proof_Context.init_global ((ThyC.Isac())) |
102 val (form', _, _, rewritten) = |
102 val (form', _, _, rewritten) = |
103 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
103 Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form; |
104 in (*the fillpat of the thm must be dedicated to id*) |
104 in (*the fillpat of the thm must be dedicated to id*) |
105 if id = erpaID andalso rewritten then |
105 if id = erpaID andalso rewritten then |
106 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
106 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
107 else NONE |
107 else NONE |
108 end |
108 end |