src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 59044 c04eccae1de8
parent 59043 a00110bdb4a3
child 59058 a78612c67ec0
--- 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;