# HG changeset patch
# User wenzelm
# Date 972926774 -3600
# Node ID 807992b67eddeb80c858a416c42b29b70445563f
# Parent  445e3b87f28bab40ad996a6920c96b07e3026f1b
tuned goals output;

diff -r 445e3b87f28b -r 807992b67edd src/Pure/Isar/isar_output.ML
--- 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;
 
diff -r 445e3b87f28b -r 807992b67edd src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Oct 30 18:25:38 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Oct 30 18:26:14 2000 +0100
@@ -43,7 +43,7 @@
   val pretty_thms: thm list -> Pretty.T
   val verbose: bool ref
   val print_state: int -> state -> unit
-  val pretty_goals: state -> bool -> Pretty.T list
+  val pretty_goals: bool -> state -> Pretty.T list
   val level: state -> int
   type method
   val method: (thm list -> tactic) -> method
@@ -352,9 +352,9 @@
       else pretty_goal (find_goal 0 state))
   in Pretty.writeln (Pretty.chunks prts) end;
 
-fun pretty_goals state print_goal =
+fun pretty_goals main_goal state =
   let val (_, (_, ((_, (_, thm)), _))) = find_goal 0 state
-  in Locale.pretty_sub_goals print_goal (!goals_limit) thm end;
+  in Locale.pretty_sub_goals main_goal (!goals_limit) thm end;