# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID c04eccae1de80b2c0ffff1b212bf253ea6829e7f
# Parent  a00110bdb4a3ffe0ac78dffdf0343957ebc4a091
tuned whitespace

diff -r a00110bdb4a3 -r c04eccae1de8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -885,8 +885,8 @@
     val ctr_specss = map #ctr_specs corec_specs;
     val corec_args = hd corecs
       |> fst o split_last o binder_types o fastype_of
-      |> map (fn T => if range_type T = HOLogic.boolT
-          then Abs (Name.uu_, domain_type T, @{term False})
+      |> map (fn T =>
+          if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False})
           else Const (@{const_name undefined}, T))
       |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
       |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;