src/Pure/drule.ML

   val MRL: thm list list * thm list -> thm list
   val MRS: thm list * thm -> thm
   val print_cterm: Sign.cterm -> unit
   val print_ctyp: Sign.ctyp -> unit
   val print_goals: int -> thm -> unit
+  val print_goals_ref: (int -> thm -> unit) ref
   val print_sg: Sign.sg -> unit
   val print_theory: theory -> unit
   val pprint_sg: Sign.sg -> pprint_args -> unit
   val pprint_theory: theory -> pprint_args -> unit
   val print_thm: thm -> unit

 	      writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
         else printgoals (1, As);
    printff tpairs
 end;
 
+(*"hook" for user interfaces: allows print_goals to be replaced*)
+val print_goals_ref = ref print_goals;
 
 (** theorem equality test is exported and used by BEST_FIRST **)
 
 (*equality of signatures means exact identity -- by ref equality*)
 fun eq_sg (sg1,sg2) = (#stamps(Sign.rep_sg sg1) = #stamps(Sign.rep_sg sg2));