tuning
authorblanchet
Fri Sep 19 13:27:04 2014 +0200 (2014-09-19)
changeset 58387bc35a30cf0f2
parent 58386 6999f55645ea
child 58388 4d408eb71301
tuning
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 19 10:40:56 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
     1.3 @@ -64,12 +64,12 @@
     1.4  open BNF_FP_Rec_Sugar_Util
     1.5  open BNF_GFP_Rec_Sugar_Tactics
     1.6  
     1.7 -val codeN = "code"
     1.8 -val ctrN = "ctr"
     1.9 -val discN = "disc"
    1.10 -val disc_iffN = "disc_iff"
    1.11 -val excludeN = "exclude"
    1.12 -val selN = "sel"
    1.13 +val codeN = "code";
    1.14 +val ctrN = "ctr";
    1.15 +val discN = "disc";
    1.16 +val disc_iffN = "disc_iff";
    1.17 +val excludeN = "exclude";
    1.18 +val selN = "sel";
    1.19  
    1.20  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
    1.21  val simp_attrs = @{attributes [simp]};
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 10:40:56 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
     2.3 @@ -75,8 +75,8 @@
     2.4  open Ctr_Sugar_General_Tactics
     2.5  open BNF_FP_Rec_Sugar_Util
     2.6  
     2.7 -val inductN = "induct"
     2.8 -val simpsN = "simps"
     2.9 +val inductN = "induct";
    2.10 +val simpsN = "simps";
    2.11  
    2.12  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
    2.13  val simp_attrs = @{attributes [simp]};
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 10:40:56 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 13:27:04 2014 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4       is_some lfp_sugar_thms, lthy)
     3.5    end;
     3.6  
     3.7 -exception NOT_A_MAP of term;
     3.8 +exception NO_MAP of term;
     3.9  
    3.10  fun ill_formed_rec_call ctxt t =
    3.11    error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
    3.12 @@ -101,20 +101,20 @@
    3.13            in
    3.14              Term.list_comb (map', fs')
    3.15            end
    3.16 -        | NONE => raise NOT_A_MAP t)
    3.17 -      | massage_map _ _ t = raise NOT_A_MAP t
    3.18 +        | NONE => raise NO_MAP t)
    3.19 +      | massage_map _ _ t = raise NO_MAP t
    3.20      and massage_map_or_map_arg U T t =
    3.21        if T = U then
    3.22          tap check_no_call t
    3.23        else
    3.24          massage_map U T t
    3.25 -        handle NOT_A_MAP _ => massage_mutual_fun U T t;
    3.26 +        handle NO_MAP _ => massage_mutual_fun U T t;
    3.27  
    3.28      fun massage_call (t as t1 $ t2) =
    3.29          if has_call t then
    3.30            if t2 = y then
    3.31              massage_map yU yT (elim_y t1) $ y'
    3.32 -            handle NOT_A_MAP t' => invalid_map ctxt t'
    3.33 +            handle NO_MAP t' => invalid_map ctxt t'
    3.34            else
    3.35              let val (g, xs) = Term.strip_comb t2 in
    3.36                if g = y then