1.1 --- a/src/Pure/drule.ML	Thu Oct 21 17:10:15 1993 +0100
     1.2 +++ b/src/Pure/drule.ML	Thu Oct 21 17:20:01 1993 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    val print_cterm: Sign.cterm -> unit
     1.5    val print_ctyp: Sign.ctyp -> unit
     1.6    val print_goals: int -> thm -> unit
     1.7 +  val print_goals_ref: (int -> thm -> unit) ref
     1.8    val print_sg: Sign.sg -> unit
     1.9    val print_theory: theory -> unit
    1.10    val pprint_sg: Sign.sg -> pprint_args -> unit
    1.11 @@ -332,6 +333,8 @@
    1.12     printff tpairs
    1.13  end;
    1.14  
    1.15 +(*"hook" for user interfaces: allows print_goals to be replaced*)
    1.16 +val print_goals_ref = ref print_goals;
    1.17  
    1.18  (** theorem equality test is exported and used by BEST_FIRST **)
    1.19  

     2.1 --- a/src/Pure/tctical.ML	Thu Oct 21 17:10:15 1993 +0100
     2.2 +++ b/src/Pure/tctical.ML	Thu Oct 21 17:20:01 1993 +0100
     2.3 @@ -179,8 +179,9 @@
     2.4  val goals_limit = ref 10;
     2.5  
     2.6  (*Print the current proof state and pass it on.*)
     2.7 -val print_tac = Tactic (fn state => 
     2.8 -  (print_goals (!goals_limit) state;   Sequence.single state));
     2.9 +val print_tac = Tactic 
    2.10 +    (fn state => 
    2.11 +     (!print_goals_ref (!goals_limit) state;   Sequence.single state));
    2.12  
    2.13  (*Pause until a line is typed -- if non-empty then fail. *)
    2.14  val pause_tac = Tactic (fn state => 
    2.15 @@ -210,7 +211,7 @@
    2.16  
    2.17  (*Extract from a tactic, a thm->thm seq function that handles tracing*)
    2.18  fun tracify flag (Tactic tf) state =
    2.19 -  if !flag then (print_goals (!goals_limit) state;  
    2.20 +  if !flag then (!print_goals_ref (!goals_limit) state;  
    2.21  		 prs"** Press RETURN to continue: ";
    2.22  		 exec_trace_command flag (tf,state))
    2.23    else tf state;