src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 57794 73052169b213
parent 57633 4ff8c090d580
child 57798 018dc778cbcc
--- 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);