src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57091 1fa9c19ba2c9
parent 57090 0224caba67ca
child 57094 589ec121ce1a
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:32:51 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:32:55 2014 +0200
     1.3 @@ -363,7 +363,8 @@
     1.4  
     1.5      val ms = map length ctr_Tss;
     1.6  
     1.7 -    fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings (k - 1)));
     1.8 +    fun can_definitely_rely_on_disc k =
     1.9 +      not (Binding.is_empty (nth raw_disc_bindings (k - 1))) orelse nth ms (k - 1) = 0;
    1.10      fun can_rely_on_disc k =
    1.11        can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
    1.12      fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
    1.13 @@ -380,8 +381,8 @@
    1.14        |> map4 (fn k => fn m => fn ctr => fn disc =>
    1.15          qualify false
    1.16            (if Binding.is_empty disc then
    1.17 -             if should_omit_disc_binding k then disc
    1.18 -             else if m = 0 then equal_binding
    1.19 +             if m = 0 then equal_binding
    1.20 +             else if should_omit_disc_binding k then disc
    1.21               else standard_disc_binding ctr
    1.22             else if Binding.eq_name (disc, standard_binding) then
    1.23               standard_disc_binding ctr
    1.24 @@ -1005,7 +1006,7 @@
    1.25    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    1.26    prepare_free_constructors Syntax.read_term;
    1.27  
    1.28 -val parse_bound_term = parse_binding --| @{keyword ":"} -- Parse.term;
    1.29 +val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
    1.30  
    1.31  val parse_ctr_options =
    1.32    Scan.optional (@{keyword "("} |-- Parse.list1
    1.33 @@ -1021,12 +1022,12 @@
    1.34    parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg --
    1.35    Scan.optional parse_defaults [];
    1.36  
    1.37 -val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term parse_binding);
    1.38 +val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term Parse.binding);
    1.39  
    1.40  val _ =
    1.41    Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    1.42      "register an existing freely generated type's constructors"
    1.43 -    (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
    1.44 +    (parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
    1.45       >> free_constructors_cmd);
    1.46  
    1.47  val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);