--- a/src/Pure/Isar/isar_output.ML Mon Oct 30 18:25:38 2000 +0100
+++ b/src/Pure/Isar/isar_output.ML Mon Oct 30 18:26:14 2000 +0100
@@ -292,18 +292,16 @@
fun pretty_thm ctxt thms =
Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
-fun pretty_goals state print_goal _ _ =
- Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state
- handle Toplevel.UNDEF
- => error "No proof state")
- print_goal);
-
fun output_with pretty src ctxt x =
let
val prt = pretty ctxt x; (*always pretty!*)
val prt' = if ! source then pretty_source src else prt;
in cond_display (cond_quote prt') end;
+fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ =>
+ Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
+ handle Toplevel.UNDEF => error "No proof state")))) src state;
+
in
val _ = add_commands
@@ -312,10 +310,8 @@
("prop", args Args.local_prop (output_with pretty_term)),
("term", args Args.local_term (output_with pretty_term)),
("typ", args Args.local_typ_no_norm (output_with pretty_typ)),
- ("goals", fn src => fn state =>
- args (Scan.succeed ()) (output_with (pretty_goals state true)) src state),
- ("subgoals", fn src => fn state =>
- args (Scan.succeed ()) (output_with (pretty_goals state false)) src state)];
+ ("goals", output_goals true),
+ ("subgoals", output_goals false)];
end;