diff -r b5965890e54d -r ef0a5fd30f3b src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -56,6 +56,8 @@
 
   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 =
@@ -174,4 +176,8 @@
 
 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;