1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 30 16:44:54 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 30 09:40:28 2014 +0200
     1.3 @@ -1237,7 +1237,14 @@
     1.4  
     1.5              val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
     1.6  
     1.7 -            val sel_default_eqs = map (prepare_term lthy) raw_sel_default_eqs;
     1.8 +            val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss;
     1.9 +            val sel_bTs =
    1.10 +              flat sel_bindingss ~~ flat sel_Tss
    1.11 +              |> filter_out (Binding.is_empty o fst)
    1.12 +              |> distinct (Binding.eq_name o pairself fst);
    1.13 +            val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
    1.14 +
    1.15 +            val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
    1.16  
    1.17              fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
    1.18              val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;

     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 30 16:44:54 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 30 09:40:28 2014 +0200
     2.3 @@ -62,6 +62,7 @@
     2.4    val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
     2.5    val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
     2.6  
     2.7 +  val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
     2.8    val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     2.9      (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
    2.10      ctr_sugar * local_theory
    2.11 @@ -334,6 +335,12 @@
    2.12        malformed ()
    2.13    end;
    2.14  
    2.15 +(* Ideally, we would enrich the context with constants rather than free variables. *)
    2.16 +fun fake_local_theory_for_sel_defaults sel_bTs =
    2.17 +  Proof_Context.allow_dummies
    2.18 +  #> Proof_Context.add_fixes (map (fn (b, T) => (b, SOME T, NoSyn)) sel_bTs)
    2.19 +  #> snd;
    2.20 +
    2.21  type ('c, 'a) ctr_spec = (binding * 'c) * 'a list;
    2.22  
    2.23  fun disc_of_ctr_spec ((disc, _), _) = disc;
    2.24 @@ -507,30 +514,35 @@
    2.25          (true, [], [], [], [], [], lthy')
    2.26        else
    2.27          let
    2.28 -          val sel_bindings = flat sel_bindingss;
    2.29 -          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
    2.30 -          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
    2.31 +          val all_sel_bindings = flat sel_bindingss;
    2.32 +          val num_all_sel_bindings = length all_sel_bindings;
    2.33 +          val uniq_sel_bindings = distinct Binding.eq_name all_sel_bindings;
    2.34 +          val all_sels_distinct = (length uniq_sel_bindings = num_all_sel_bindings);
    2.35  
    2.36            val sel_binding_index =
    2.37 -            if all_sels_distinct then 1 upto length sel_bindings
    2.38 -            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
    2.39 +            if all_sels_distinct then
    2.40 +              1 upto num_all_sel_bindings
    2.41 +            else
    2.42 +              map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings;
    2.43  
    2.44 -          val all_proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
    2.45 +          val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
    2.46            val sel_infos =
    2.47              AList.group (op =) (sel_binding_index ~~ all_proto_sels)
    2.48              |> sort (int_ord o pairself fst)
    2.49              |> map snd |> curry (op ~~) uniq_sel_bindings;
    2.50            val sel_bindings = map fst sel_infos;
    2.51 -          val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
    2.52 -
    2.53 -          val sel_default_lthy = no_defs_lthy
    2.54 -            |> Proof_Context.allow_dummies
    2.55 -            |> Proof_Context.add_fixes
    2.56 -              (map2 (fn b => fn T => (b, SOME T, NoSyn)) sel_bindings sel_Ts)
    2.57 -            |> snd;
    2.58  
    2.59            val sel_defaults =
    2.60 -            map (extract_sel_default sel_default_lthy o prep_term sel_default_lthy) sel_default_eqs;
    2.61 +            if null sel_default_eqs then
    2.62 +              []
    2.63 +            else
    2.64 +              let
    2.65 +                val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
    2.66 +                val fake_lthy =
    2.67 +                  fake_local_theory_for_sel_defaults (sel_bindings ~~ sel_Ts) no_defs_lthy;
    2.68 +              in
    2.69 +                map (extract_sel_default fake_lthy o prep_term fake_lthy) sel_default_eqs
    2.70 +              end;
    2.71  
    2.72            fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
    2.73