# HG changeset patch
# User wenzelm
# Date 911647086 -3600
# Node ID 63184e276c1d1dfd1dc51a4f904ec74622b65b47
# Parent  dcc446da8e19a8cb43184b622786d7a8ec4e3bbc
print_state: use begin_goal from Goals.current_goals_markers;

diff -r dcc446da8e19 -r 63184e276c1d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Nov 21 12:17:18 1998 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Nov 21 12:18:06 1998 +0100
@@ -266,6 +266,7 @@
 
 fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   let
+    val ref (_, _, begin_goal) = Goals.current_goals_markers;
     val prt_tthm = Attribute.pretty_tthm;
 
     fun print_facts None = ()
@@ -277,7 +278,7 @@
 
     fun print_goal (i, ((kind, name, _, _), (_, thm))) =
       (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":");	(* FIXME *)
-        Locale.print_goals (! goals_limit) thm);
+        Locale.print_goals_marker begin_goal (! goals_limit) thm);
   in
     writeln ("Nesting level: " ^ string_of_int (length nodes div 1));	(* FIXME *)
     writeln "";