src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57090 0224caba67ca
parent 57038 2114f3224b2c
child 57091 1fa9c19ba2c9
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 14:15:48 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:32:51 2014 +0200
     1.3 @@ -368,6 +368,8 @@
     1.4        can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
     1.5      fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
     1.6  
     1.7 +    val equal_binding = @{binding "="};
     1.8 +
     1.9      fun is_disc_binding_valid b =
    1.10        not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
    1.11  
    1.12 @@ -378,10 +380,9 @@
    1.13        |> map4 (fn k => fn m => fn ctr => fn disc =>
    1.14          qualify false
    1.15            (if Binding.is_empty disc then
    1.16 -             if should_omit_disc_binding k then disc else standard_disc_binding ctr
    1.17 -           else if Binding.eq_name (disc, equal_binding) then
    1.18 -             if m = 0 then disc
    1.19 -             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
    1.20 +             if should_omit_disc_binding k then disc
    1.21 +             else if m = 0 then equal_binding
    1.22 +             else standard_disc_binding ctr
    1.23             else if Binding.eq_name (disc, standard_binding) then
    1.24               standard_disc_binding ctr
    1.25             else