--- 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;
--- 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;