equal
deleted
inserted
replaced
218 Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state"; |
218 Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state"; |
219 val res = |
219 val res = |
220 (finish ctxt' st |
220 (finish ctxt' st |
221 |> Drule.flexflex_unique |
221 |> Drule.flexflex_unique |
222 |> Thm.check_shyps sorts |
222 |> Thm.check_shyps sorts |
223 (* |> Thm.check_hyps ctxt' *) (* FIXME *)) |
223 (* |> Thm.check_hyps (Context.Proof ctxt') *) (* FIXME *)) |
224 handle THM (msg, _, _) => err msg | ERROR msg => err msg; |
224 handle THM (msg, _, _) => err msg | ERROR msg => err msg; |
225 in |
225 in |
226 if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res |
226 if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res |
227 else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res)) |
227 else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res)) |
228 end); |
228 end); |