--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Aug 05 11:07:53 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Aug 05 13:52:35 2014 +0200
@@ -124,10 +124,10 @@
distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
(T_name0,
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
- inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
- rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
- case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
- split_asm = split_asm});
+ inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
+ rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+ case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
+ split_asm = split_asm});
val infos = map_index mk_info (take nn_fp fp_sugars);