--- 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]};
--- 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]};
--- 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