# 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