# HG changeset patch
# User wenzelm
# Date 999972332 -7200
# Node ID 07a9d5db83217186e333a9f21a10edce8a7a2fe3
# Parent  685daff01da4203a71e0404783b2adb03e55a915
export pretty_goals;

diff -r 685daff01da4 -r 07a9d5db8321 src/Pure/locale.ML
--- a/src/Pure/locale.ML	Sat Sep 08 20:05:14 2001 +0200
+++ b/src/Pure/locale.ML	Sat Sep 08 20:05:32 2001 +0200
@@ -21,6 +21,7 @@
 sig
   val print_locales: theory -> unit
   val pretty_goals_marker: string -> int -> thm -> Pretty.T list
+  val pretty_goals: int -> thm -> Pretty.T list
   val pretty_sub_goals: bool -> int -> thm -> Pretty.T list
   val print_goals_marker: string -> int -> thm -> unit
   val print_goals: int -> thm -> unit
@@ -588,8 +589,6 @@
   fun vars_of t = sort_idxs (add_vars (t, []));
   fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
 
-in
-
   fun pretty_goals_marker_aux begin_goal print_msg print_goal maxgoals state =
     let
       val {sign, ...} = rep_thm state;
@@ -651,12 +650,12 @@
      (! show_types orelse ! show_sorts, ! show_sorts)
   end;
 
+in
   fun pretty_goals_marker bg = pretty_goals_marker_aux bg true true;
   val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
-
   val pretty_sub_goals = pretty_goals_marker_aux "" false;
+  val pretty_goals = pretty_goals_marker "";
   val print_goals = print_goals_marker "";
-
 end;