# HG changeset patch
# User blanchet
# Date 1382111245 -7200
# Node ID 0af35cebe8cacc952ea4055d932daef1efa390d8
# Parent  5874be04e1f902ed7c176957ff0a5afcc03895a5
don't print BNF constants

diff -r 5874be04e1f9 -r 0af35cebe8ca src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Oct 18 16:02:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Oct 18 17:47:25 2013 +0200
@@ -841,12 +841,6 @@
     val rel = mk_bnf_rel pred2RTs CA' CB';
     val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
 
-    val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
-        raw_wit_defs @ [raw_rel_def]) of
-        [] => ()
-      | defs => Proof_Display.print_consts true lthy_old (K false)
-          (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
-
     val map_id0_goal =
       let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
         mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')