equal
deleted
inserted
replaced
95 C |
95 C |
96 *) |
96 *) |
97 fun check_finished ctxt th = |
97 fun check_finished ctxt th = |
98 if Thm.no_prems th then th |
98 if Thm.no_prems th then th |
99 else |
99 else |
100 raise THM ("Proof failed.\n" ^ |
100 raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]); |
101 Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]); |
|
102 |
101 |
103 fun finish ctxt = check_finished ctxt #> conclude; |
102 fun finish ctxt = check_finished ctxt #> conclude; |
104 |
103 |
105 |
104 |
106 |
105 |