author blanchet Mon May 26 16:32:51 2014 +0200 (2014-05-26) changeset 57090 0224caba67ca parent 57089 353652f47974 child 57091 1fa9c19ba2c9
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
```     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 ":"};
```