# HG changeset patch
# User blanchet
# Date 1401114771 -7200
# Node ID 0224caba67caa4f7b9c507729431bb852c753860
# Parent  353652f479742cf17e4cc0f0dca5c9fbf3801aff
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax

diff -r 353652f47974 -r 0224caba67ca src/HOL/BNF_Examples/Misc_Primcorec.thy
--- a/src/HOL/BNF_Examples/Misc_Primcorec.thy	Mon May 26 14:15:48 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy	Mon May 26 16:32:51 2014 +0200
@@ -56,7 +56,7 @@
   "un_J112 (j1_sum _) = j1_sum 0" |
   "un_J121 (j1_sum n) = n + 1" |
   "un_J122 (j1_sum n) = j2_sum (n + 1)" |
-  "n = 0 \<Longrightarrow> is_J21 (j2_sum n)" |
+  "n = 0 \<Longrightarrow> j2_sum n = J21" |
   "un_J221 (j2_sum n) = j1_sum (n + 1)" |
   "un_J222 (j2_sum n) = j2_sum (n + 1)"
 
diff -r 353652f47974 -r 0224caba67ca src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 14:15:48 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:32:51 2014 +0200
@@ -368,6 +368,8 @@
       can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
     fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
 
+    val equal_binding = @{binding "="};
+
     fun is_disc_binding_valid b =
       not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
 
@@ -378,10 +380,9 @@
       |> map4 (fn k => fn m => fn ctr => fn disc =>
         qualify false
           (if Binding.is_empty disc then
-             if should_omit_disc_binding k then disc else standard_disc_binding ctr
-           else if Binding.eq_name (disc, equal_binding) then
-             if m = 0 then disc
-             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
+             if should_omit_disc_binding k then disc
+             else if m = 0 then equal_binding
+             else standard_disc_binding ctr
            else if Binding.eq_name (disc, standard_binding) then
              standard_disc_binding ctr
            else
diff -r 353652f47974 -r 0224caba67ca src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon May 26 14:15:48 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon May 26 16:32:51 2014 +0200
@@ -66,7 +66,6 @@
   val certify: Proof.context -> term -> cterm
 
   val standard_binding: binding
-  val equal_binding: binding
   val parse_binding: binding parser
   val parse_binding_colon: binding parser
   val parse_opt_binding_colon: binding parser
@@ -234,7 +233,6 @@
    "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
    binding at all, depending on the context. *)
 val standard_binding = @{binding _};
-val equal_binding = @{binding "="};
 
 val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
 val parse_binding_colon = parse_binding --| @{keyword ":"};