src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML

 
   val mk_co_rec: theory -> fp_kind -> typ list -> typ -> term -> term
 
   val mk_conjunctN: int -> int -> thm
   val conj_dests: int -> thm -> thm list
+
+  val print_def_consts: bool -> (term * (string * thm)) list -> Proof.context -> unit
 end;
 
 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
 struct
 

   | mk_conjunctN 2 2 = conjunct2
   | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1));
 
 fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n);
 
+fun print_def_consts int defs ctxt =
+  Proof_Display.print_consts int (Position.thread_data ()) ctxt (K false)
+    (map_filter (try (dest_Free o fst)) defs);
+
 end;