--- 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);
--- 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