# HG changeset patch
# User blanchet
# Date 1407239555 -7200
# Node ID 73052169b21383bcf4b28ac11150ebc6df52f63d
# Parent  d1cf76cef93bb0f8e546757a8fc4f50e68fc382e
tuning whitespace

diff -r d1cf76cef93b -r 73052169b213 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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);