# HG changeset patch
# User blanchet
# Date 1401116318 -7200
# Node ID c46fe1cb1d9418d9b9bc8c061aa33b057e4120bb
# Parent  59603f4f1d2ec36708923e42a211a83cbc0f49b4
don't conceal (co)datatypes

diff -r 59603f4f1d2e -r c46fe1cb1d94 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon May 26 16:33:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon May 26 16:58:38 2014 +0200
@@ -1267,7 +1267,7 @@
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
       |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
-        typedef (Binding.conceal b, params, mx) car_final NONE
+        typedef (b, params, mx) car_final NONE
           (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
       |>> apsnd split_list o split_list;
 
diff -r 59603f4f1d2e -r c46fe1cb1d94 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon May 26 16:33:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon May 26 16:58:38 2014 +0200
@@ -860,7 +860,7 @@
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
       |> fold_map3 (fn b => fn mx => fn car_init =>
-        typedef (Binding.conceal b, params, mx) car_init NONE
+        typedef (b, params, mx) car_init NONE
           (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
             rtac alg_init_thm] 1)) bs mixfixes car_inits
       |>> apsnd split_list o split_list;