1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -157,8 +157,8 @@
     1.4      val casex = mk_case As B;
     1.5      val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
     1.6  
     1.7 -    val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
     1.8 -      mk_Freess "x" ctr_Tss
     1.9 +    val ((((((((xss, xss'), yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
    1.10 +      mk_Freess' "x" ctr_Tss
    1.11        ||>> mk_Freess "y" ctr_Tss
    1.12        ||>> mk_Frees "f" case_Ts
    1.13        ||>> mk_Frees "g" case_Ts
    1.14 @@ -206,16 +206,19 @@
    1.15  
    1.16            fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k));
    1.17  
    1.18 +          fun mk_default T t =
    1.19 +            let
    1.20 +              val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []);
    1.21 +              val Ts = map TFree (Term.add_tfreesT T []);
    1.22 +            in Term.subst_atomic_types (Ts0 ~~ Ts) t end;
    1.23 +
    1.24            fun mk_sel_case_args b proto_sels T =
    1.25              map2 (fn Ts => fn k =>
    1.26                (case AList.lookup (op =) proto_sels k of
    1.27                  NONE =>
    1.28 -                let val def_T = Ts ---> T in
    1.29 -                  (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
    1.30 -                    NONE => mk_undefined def_T
    1.31 -                  | SOME t => fold_rev (fn T => Term.lambda (Free (Name.uu, T))) Ts
    1.32 -                      (Term.subst_atomic_types [(fastype_of t, T)] t))
    1.33 -                end
    1.34 +                (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
    1.35 +                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
    1.36 +                | SOME t => mk_default (Ts ---> T) t)
    1.37                | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
    1.38  
    1.39            fun sel_spec b proto_sels =
    1.40 @@ -355,20 +358,23 @@
    1.41              ([], [], [], [], [], [], [], [])
    1.42            else
    1.43              let
    1.44 -              fun make_sel_thm case_thm sel_def = case_thm RS (sel_def RS trans);
    1.45 +              fun make_sel_thm xs' case_thm sel_def =
    1.46 +                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
    1.47 +                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
    1.48  
    1.49                fun has_undefined_rhs thm =
    1.50                  (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
    1.51                    Const (@{const_name undefined}, _) => true
    1.52                  | _ => false);
    1.53  
    1.54 -              val sel_thmss = map2 (map o make_sel_thm) case_thms sel_defss;
    1.55 +              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
    1.56  
    1.57                val all_sel_thms =
    1.58                  (if all_sels_distinct andalso forall null sel_defaultss then
    1.59                     flat sel_thmss
    1.60                   else
    1.61 -                   map_product (fn s => fn c => make_sel_thm c s) sel_defs case_thms)
    1.62 +                   map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
    1.63 +                     (xss' ~~ case_thms))
    1.64                  |> filter_out has_undefined_rhs;
    1.65  
    1.66                fun mk_unique_disc_def () =