src/Pure/locale.ML

--- a/src/Pure/locale.ML	Thu Oct 22 12:35:40 1998 +0200
+++ b/src/Pure/locale.ML	Thu Oct 22 20:07:42 1998 +0200
@@ -19,6 +19,7 @@
 sig
   val print_locales: theory -> unit
   val print_goals: int -> thm -> unit
+  val print_goals_marker: string -> int -> thm -> unit
 end;
 
 signature LOCALE =
@@ -476,7 +477,7 @@
 
 in
 
-  fun print_goals maxgoals state =
+  fun print_goals_marker begin_goal maxgoals state =
     let
       val {sign, ...} = rep_thm state;
 
@@ -505,7 +506,7 @@
 
       fun print_subgoals (_, []) = ()
         | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
-            [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A]));
+            [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]));
               print_subgoals (n + 1, As));
 
       val print_ffpairs =
@@ -540,6 +541,8 @@
      (! show_types orelse ! show_sorts, ! show_sorts)
   end;
 
+  val print_goals = print_goals_marker "";
+
 end;