equal
deleted
inserted
replaced
212 (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of |
212 (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of |
213 NONE => err "Tactic failed" |
213 NONE => err "Tactic failed" |
214 | SOME st => |
214 | SOME st => |
215 let |
215 let |
216 val _ = |
216 val _ = |
217 Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state"; |
217 Theory.subthy (Thm.theory_of_thm st, thy) orelse |
|
218 err "Bad background theory of goal state"; |
218 val res = |
219 val res = |
219 (finish ctxt' st |
220 (finish ctxt' st |
220 |> Drule.flexflex_unique (SOME ctxt') |
221 |> Drule.flexflex_unique (SOME ctxt') |
221 |> Thm.check_shyps sorts |
222 |> Thm.check_shyps sorts |
222 |> Thm.check_hyps (Context.Proof ctxt')) |
223 |> Thm.check_hyps (Context.Proof ctxt')) |