src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57094 589ec121ce1a
parent 57091 1fa9c19ba2c9
child 57200 aab87ffa60cc
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:58:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue May 27 17:32:42 2014 +0200
     1.3 @@ -322,7 +322,7 @@
     1.4  fun args_of_ctr_spec ((_, args), _) = args;
     1.5  fun sel_defaults_of_ctr_spec (_, ds) = ds;
     1.6  
     1.7 -fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs)
     1.8 +fun prepare_free_constructors prep_term (((discs_sels, no_code), raw_case_binding), ctr_specs)
     1.9      no_defs_lthy =
    1.10    let
    1.11      (* TODO: sanity checks on arguments *)
    1.12 @@ -481,6 +481,11 @@
    1.13             if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
    1.14           end);
    1.15  
    1.16 +    val no_discs_sels =
    1.17 +      not discs_sels andalso
    1.18 +      forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso
    1.19 +      forall null raw_sel_defaultss;
    1.20 +
    1.21      val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
    1.22        if no_discs_sels then
    1.23          (true, [], [], [], [], [], lthy')
    1.24 @@ -1010,7 +1015,7 @@
    1.25  
    1.26  val parse_ctr_options =
    1.27    Scan.optional (@{keyword "("} |-- Parse.list1
    1.28 -        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    1.29 +        (Parse.reserved "discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    1.30        @{keyword ")"}
    1.31        >> (fn js => (member (op =) js 0, member (op =) js 1)))
    1.32      (false, false);