# HG changeset patch
# User wenzelm
# Date 873987363 -7200
# Node ID 3384c6f1f095e071ff3fcebba8cddcf9ede58d10
# Parent  a39baf59ea47aa4908e52607f895e8c47eec69e4
removed print_goals_ref (which was broken anyway);

diff -r a39baf59ea47 -r 3384c6f1f095 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Sep 11 12:24:28 1997 +0200
+++ b/src/Pure/display.ML	Thu Sep 11 16:16:03 1997 +0200
@@ -17,7 +17,6 @@
   val print_cterm	: cterm -> unit
   val print_ctyp	: ctyp -> unit
   val print_goals	: int -> thm -> unit
-  val print_goals_ref	: (int -> thm -> unit) ref
   val print_syntax	: theory -> unit
   val print_theory	: theory -> unit
   val print_thm		: thm -> unit
@@ -209,9 +208,6 @@
   end;
 
 
-(*"hook" for user interfaces: allows print_goals to be replaced*)	(* FIXME remove!? *)
-val print_goals_ref = ref print_goals;
-
 end;
 
 open Display;
diff -r a39baf59ea47 -r 3384c6f1f095 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Sep 11 12:24:28 1997 +0200
+++ b/src/Pure/goals.ML	Thu Sep 11 16:16:03 1997 +0200
@@ -120,10 +120,10 @@
 
 (*Default action is to print an error message; could be suppressed for
   special applications.*)
-fun result_error_default state msg : thm = 
-  (writeln ("Bad final proof state:");
-   !print_goals_ref (!goals_limit) state;
-   writeln msg; raise ERROR);
+fun result_error_default state msg : thm =
+ (writeln "Bad final proof state:";
+  print_goals (!goals_limit) state;
+  writeln msg; raise ERROR);
 
 val result_error_fn = ref result_error_default;
 
@@ -235,7 +235,7 @@
 
 (*Print goals of current level*)
 fun print_current_goals_default n max th =
-  (writeln ("Level " ^ string_of_int n); !print_goals_ref max th);
+  (writeln ("Level " ^ string_of_int n); print_goals max th);
 
 val print_current_goals_fn = ref print_current_goals_default;
 
diff -r a39baf59ea47 -r 3384c6f1f095 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Thu Sep 11 12:24:28 1997 +0200
+++ b/src/Pure/tctical.ML	Thu Sep 11 16:16:03 1997 +0200
@@ -192,7 +192,7 @@
 (*Print the current proof state and pass it on.*)
 val print_tac = 
     (fn st => 
-     (!print_goals_ref (!goals_limit) st;   Sequence.single st));
+     (print_goals (!goals_limit) st; Sequence.single st));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =  
@@ -229,7 +229,7 @@
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing)
-           then (!print_goals_ref (!goals_limit) st;  
+           then (print_goals (!goals_limit) st;
                  prs"** Press RETURN to continue: ";
                  exec_trace_command flag (tac,st))
   else tac st;