equal
deleted
inserted
replaced
291 |
291 |
292 fun pretty_thm ctxt thms = |
292 fun pretty_thm ctxt thms = |
293 Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms); |
293 Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms); |
294 |
294 |
295 fun pretty_goals state _ _ = |
295 fun pretty_goals state _ _ = |
296 Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state)); |
296 Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state handle Toplevel.UNDEF => |
|
297 error "No proof state")); |
297 |
298 |
298 |
299 |
299 fun output_with pretty src ctxt x = |
300 fun output_with pretty src ctxt x = |
300 let |
301 let |
301 val prt = pretty ctxt x; (*always pretty!*) |
302 val prt = pretty ctxt x; (*always pretty!*) |