equal
deleted
inserted
replaced
472 fun conclude_goal ctxt goal propss = |
472 fun conclude_goal ctxt goal propss = |
473 let |
473 let |
474 val thy = Proof_Context.theory_of ctxt; |
474 val thy = Proof_Context.theory_of ctxt; |
475 |
475 |
476 val _ = |
476 val _ = |
477 Theory.subthy (theory_of_thm goal, thy) orelse error "Bad background theory of goal state"; |
477 Theory.subthy (Thm.theory_of_thm goal, thy) orelse |
|
478 error "Bad background theory of goal state"; |
478 val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); |
479 val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); |
479 |
480 |
480 fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); |
481 fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); |
481 |
482 |
482 val th = |
483 val th = |