changeset 57093 | c46fe1cb1d94 |
parent 56766 | ba2fa4e99729 |
child 57567 | d554b0097ad4 |
--- 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;