# HG changeset patch
# User blanchet
# Date 1411126024 -7200
# Node ID bc35a30cf0f28f153a9a25fd6f246d487d3208f6
# Parent  6999f55645ead1f33c68b1b21d4c27653a7838ba
tuning

diff -r 6999f55645ea -r bc35a30cf0f2 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 19 10:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -64,12 +64,12 @@
 open BNF_FP_Rec_Sugar_Util
 open BNF_GFP_Rec_Sugar_Tactics
 
-val codeN = "code"
-val ctrN = "ctr"
-val discN = "disc"
-val disc_iffN = "disc_iff"
-val excludeN = "exclude"
-val selN = "sel"
+val codeN = "code";
+val ctrN = "ctr";
+val discN = "disc";
+val disc_iffN = "disc_iff";
+val excludeN = "exclude";
+val selN = "sel";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
diff -r 6999f55645ea -r bc35a30cf0f2 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 10:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -75,8 +75,8 @@
 open Ctr_Sugar_General_Tactics
 open BNF_FP_Rec_Sugar_Util
 
-val inductN = "induct"
-val simpsN = "simps"
+val inductN = "induct";
+val simpsN = "simps";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
diff -r 6999f55645ea -r bc35a30cf0f2 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 10:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -57,7 +57,7 @@
      is_some lfp_sugar_thms, lthy)
   end;
 
-exception NOT_A_MAP of term;
+exception NO_MAP of term;
 
 fun ill_formed_rec_call ctxt t =
   error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
@@ -101,20 +101,20 @@
           in
             Term.list_comb (map', fs')
           end
-        | NONE => raise NOT_A_MAP t)
-      | massage_map _ _ t = raise NOT_A_MAP t
+        | NONE => raise NO_MAP t)
+      | massage_map _ _ t = raise NO_MAP t
     and massage_map_or_map_arg U T t =
       if T = U then
         tap check_no_call t
       else
         massage_map U T t
-        handle NOT_A_MAP _ => massage_mutual_fun U T t;
+        handle NO_MAP _ => massage_mutual_fun U T t;
 
     fun massage_call (t as t1 $ t2) =
         if has_call t then
           if t2 = y then
             massage_map yU yT (elim_y t1) $ y'
-            handle NOT_A_MAP t' => invalid_map ctxt t'
+            handle NO_MAP t' => invalid_map ctxt t'
           else
             let val (g, xs) = Term.strip_comb t2 in
               if g = y then