src/Pure/drule.ML
changeset 67 8380bc0adde7
parent 11 d0e17c42dbb4
child 199 ac55692ab41f
--- a/src/Pure/drule.ML	Thu Oct 21 17:10:15 1993 +0100
+++ b/src/Pure/drule.ML	Thu Oct 21 17:20:01 1993 +0100
@@ -36,6 +36,7 @@
   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
@@ -332,6 +333,8 @@
    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 **)