1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 11:41:04 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 11:42:11 2012 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val mk_half_pairss: 'a list -> ('a * 'a) list list
     1.6    val mk_ctr: typ list -> term -> term
     1.7 +  val base_name_of_ctr: term -> string
     1.8    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     1.9      ((bool * term list) * term) *
    1.10        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    1.11 @@ -69,14 +70,14 @@
    1.12      Term.subst_atomic_types (Ts0 ~~ Ts) ctr
    1.13    end;
    1.14  
    1.15 -fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    1.16 -
    1.17  fun base_name_of_ctr c =
    1.18    Long_Name.base_name (case head_of c of
    1.19        Const (s, _) => s
    1.20      | Free (s, _) => s
    1.21      | _ => error "Cannot extract name of constructor");
    1.22  
    1.23 +fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    1.24 +
    1.25  fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
    1.26      (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    1.27    let
    1.28 @@ -176,8 +177,8 @@
    1.29      val xfs = map2 (curry Term.list_comb) fs xss;
    1.30      val xgs = map2 (curry Term.list_comb) gs xss;
    1.31  
    1.32 -    val eta_fs = map2 eta_expand_case_arg xss xfs;
    1.33 -    val eta_gs = map2 eta_expand_case_arg xss xgs;
    1.34 +    val eta_fs = map2 eta_expand_arg xss xfs;
    1.35 +    val eta_gs = map2 eta_expand_arg xss xgs;
    1.36  
    1.37      val fcase = Term.list_comb (casex, eta_fs);
    1.38      val gcase = Term.list_comb (casex, eta_gs);
    1.39 @@ -557,8 +558,8 @@
    1.40              (split_thm, split_asm_thm)
    1.41            end;
    1.42  
    1.43 +        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.44          val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
    1.45 -        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.46  
    1.47          val notes =
    1.48            [(case_congN, [case_cong_thm], []),