# HG changeset patch # User blanchet # Date 1425977356 -3600 # Node ID c875b71086a3d5f1a6b4420878bb3b9d1ec85ca3 # Parent c3b76f2bafbdf6cfdba3d101d6d1c9611b30998f tuning diff -r c3b76f2bafbd -r c875b71086a3 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 09 21:30:42 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Mar 10 09:49:16 2015 +0100 @@ -34,7 +34,7 @@ open BNF_FP_Def_Sugar open BNF_FP_N2M -val n2mN = "n2m_" +val n2mN = "n2m_"; type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option); diff -r c3b76f2bafbd -r c875b71086a3 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 09 21:30:42 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 10 09:49:16 2015 +0100 @@ -1052,14 +1052,10 @@ (tag_list 0 (map snd specs)) of_specs_opt [] |> flat o fst; - val _ = - let - val missing = fun_names - |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data - |> not oo member (op =)); - in - null missing orelse error ("Missing equations for " ^ commas missing) - end; + val missing = fun_names + |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data + |> not oo member (op =)); + val _ = null missing orelse error ("Missing equations for " ^ commas missing); val callssss = map_filter (try (fn Sel x => x)) eqns_data