use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
authorblanchet
Mon May 26 16:32:51 2014 +0200 (2014-05-26)
changeset 570900224caba67ca
parent 57089 353652f47974
child 57091 1fa9c19ba2c9
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
src/HOL/BNF_Examples/Misc_Primcorec.thy
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/BNF_Examples/Misc_Primcorec.thy	Mon May 26 14:15:48 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy	Mon May 26 16:32:51 2014 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    "un_J112 (j1_sum _) = j1_sum 0" |
     1.5    "un_J121 (j1_sum n) = n + 1" |
     1.6    "un_J122 (j1_sum n) = j2_sum (n + 1)" |
     1.7 -  "n = 0 \<Longrightarrow> is_J21 (j2_sum n)" |
     1.8 +  "n = 0 \<Longrightarrow> j2_sum n = J21" |
     1.9    "un_J221 (j2_sum n) = j1_sum (n + 1)" |
    1.10    "un_J222 (j2_sum n) = j2_sum (n + 1)"
    1.11  
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 14:15:48 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:32:51 2014 +0200
     2.3 @@ -368,6 +368,8 @@
     2.4        can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
     2.5      fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
     2.6  
     2.7 +    val equal_binding = @{binding "="};
     2.8 +
     2.9      fun is_disc_binding_valid b =
    2.10        not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
    2.11  
    2.12 @@ -378,10 +380,9 @@
    2.13        |> map4 (fn k => fn m => fn ctr => fn disc =>
    2.14          qualify false
    2.15            (if Binding.is_empty disc then
    2.16 -             if should_omit_disc_binding k then disc else standard_disc_binding ctr
    2.17 -           else if Binding.eq_name (disc, equal_binding) then
    2.18 -             if m = 0 then disc
    2.19 -             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
    2.20 +             if should_omit_disc_binding k then disc
    2.21 +             else if m = 0 then equal_binding
    2.22 +             else standard_disc_binding ctr
    2.23             else if Binding.eq_name (disc, standard_binding) then
    2.24               standard_disc_binding ctr
    2.25             else
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon May 26 14:15:48 2014 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon May 26 16:32:51 2014 +0200
     3.3 @@ -66,7 +66,6 @@
     3.4    val certify: Proof.context -> term -> cterm
     3.5  
     3.6    val standard_binding: binding
     3.7 -  val equal_binding: binding
     3.8    val parse_binding: binding parser
     3.9    val parse_binding_colon: binding parser
    3.10    val parse_opt_binding_colon: binding parser
    3.11 @@ -234,7 +233,6 @@
    3.12     "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
    3.13     binding at all, depending on the context. *)
    3.14  val standard_binding = @{binding _};
    3.15 -val equal_binding = @{binding "="};
    3.16  
    3.17  val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
    3.18  val parse_binding_colon = parse_binding --| @{keyword ":"};