1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon May 26 16:33:06 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon May 26 16:58:38 2014 +0200
     1.3 @@ -1267,7 +1267,7 @@
     1.4      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
     1.5        lthy
     1.6        |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
     1.7 -        typedef (Binding.conceal b, params, mx) car_final NONE
     1.8 +        typedef (b, params, mx) car_final NONE
     1.9            (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
    1.10        |>> apsnd split_list o split_list;
    1.11  

     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon May 26 16:33:06 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon May 26 16:58:38 2014 +0200
     2.3 @@ -860,7 +860,7 @@
     2.4      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
     2.5        lthy
     2.6        |> fold_map3 (fn b => fn mx => fn car_init =>
     2.7 -        typedef (Binding.conceal b, params, mx) car_init NONE
     2.8 +        typedef (b, params, mx) car_init NONE
     2.9            (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
    2.10              rtac alg_init_thm] 1)) bs mixfixes car_inits
    2.11        |>> apsnd split_list o split_list;