--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 28 17:11:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 28 18:44:50 2013 +0200
@@ -1119,8 +1119,8 @@
xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
lthy)) =
- fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
- no_defs_lthy0;
+ fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
+ fake_Ts fp_eqs no_defs_lthy0;
val time = time lthy;
val timer = time (Timer.startRealTimer ());