# HG changeset patch
# User lcp
# Date 751282279 -3600
# Node ID d8f3807649346d0cdc81c33c0fbdf41eb673b77f
# Parent  8380bc0adde7e5a793cddfb76a60daa37b034af7
goals/print_top,prepare_proof: now call \!print_goals_ref

diff -r 8380bc0adde7 -r d8f380764934 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Oct 21 17:20:01 1993 +0100
+++ b/src/Pure/goals.ML	Fri Oct 22 10:31:19 1993 +0100
@@ -133,7 +133,7 @@
       and st0 = c_rew (trivial (Sign.cterm_of sign B))
       fun result_error state msg = 
         (writeln ("Bad final proof state:");
- 	 print_goals (!goals_limit) state;
+ 	 !print_goals_ref (!goals_limit) state;
 	 error msg)
       (*discharges assumptions from state in the order they appear in goal;
 	checks (if requested) that resulting theorem is equivalent to goal. *)
@@ -226,7 +226,7 @@
 (*Print a level of the goal stack.*)
 fun print_top ((th,_), pairs) = 
    (prs("Level " ^ string_of_int(length pairs) ^ "\n"); 
-    print_goals (!goals_limit) th);
+    !print_goals_ref (!goals_limit) th);
 
 (*Printing can raise exceptions, so the assignment occurs last.
   Can do   setstate[(st,Sequence.null)]  to set st as the state.  *)