avoid fragile Sign.intern_const -- pass internal names directly;
authorwenzelm
Wed Dec 14 21:54:32 2011 +0100 (2011-12-14)
changeset 4587971b8d0d170b1
parent 45878 2dad374cf440
child 45880 061ef175f7a1
avoid fragile Sign.intern_const -- pass internal names directly;
tuned;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 20:36:17 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 21:54:32 2011 +0100
     1.3 @@ -2045,7 +2045,7 @@
     1.4               resolve_tac rec_intrs 1,
     1.5               REPEAT (solve (prems @ rec_total_thms) prems 1)])
     1.6        end) (rec_eq_prems ~~
     1.7 -        Datatype_Prop.make_primrecs new_type_names descr' thy12);
     1.8 +        Datatype_Prop.make_primrecs reccomb_names descr' thy12);
     1.9  
    1.10      val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms)
    1.11        (descr1 ~~ distinct_thms ~~ inject_thms);
     2.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 20:36:17 2011 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 21:54:32 2011 +0100
     2.3 @@ -199,10 +199,9 @@
     2.4      (*********************** definition of constructors ***********************)
     2.5  
     2.6      val big_rep_name = big_name ^ "_Rep_";
     2.7 -    val rep_names = map (prefix "Rep_") new_type_names;
     2.8      val rep_names' = map (fn i => big_rep_name ^ string_of_int i) (1 upto length (flat (tl descr)));
     2.9      val all_rep_names =
    2.10 -      map (Sign.intern_const thy3) rep_names @
    2.11 +      map (#Rep_name o #1 o #2) typedefs @
    2.12        map (Sign.full_bname thy3) rep_names';
    2.13  
    2.14      (* isomorphism declarations *)
    2.15 @@ -212,7 +211,8 @@
    2.16  
    2.17      (* constructor definitions *)
    2.18  
    2.19 -    fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
    2.20 +    fun make_constr_def tname (typedef: Typedef.info) T n
    2.21 +        ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
    2.22        let
    2.23          fun constr_arg dt (j, l_args, r_args) =
    2.24            let
    2.25 @@ -224,19 +224,18 @@
    2.26                  (j + 1, free_t :: l_args, mk_lim
    2.27                    (Const (nth all_rep_names m, U --> Univ_elT) $
    2.28                      Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
    2.29 -            | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
    2.30 +            | _ => (j + 1, free_t :: l_args, (Leaf $ mk_inj T free_t) :: r_args))
    2.31            end;
    2.32  
    2.33          val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
    2.34          val constrT = map (Datatype_Aux.typ_of_dtyp descr') cargs ---> T;
    2.35 -        val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    2.36 -        val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    2.37 +        val ({Abs_name, Rep_name, ...}, _) = typedef;
    2.38          val lhs = list_comb (Const (cname, constrT), l_args);
    2.39          val rhs = mk_univ_inj r_args n i;
    2.40 -        val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
    2.41 +        val def = Logic.mk_equals (lhs, Const (Abs_name, Univ_elT --> T) $ rhs);
    2.42          val def_name = Long_Name.base_name cname ^ "_def";
    2.43          val eqn =
    2.44 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
    2.45 +          HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
    2.46          val ([def_thm], thy') =
    2.47            thy
    2.48            |> Sign.add_consts_i [(cname', constrT, mx)]
    2.49 @@ -246,12 +245,11 @@
    2.50  
    2.51      (* constructor definitions for datatype *)
    2.52  
    2.53 -    fun dt_constr_defs ((((_, (_, _, constrs)), tname), T), constr_syntax)
    2.54 +    fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax)
    2.55          (thy, defs, eqns, rep_congs, dist_lemmas) =
    2.56        let
    2.57          val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
    2.58 -        val rep_const =
    2.59 -          cterm_of thy (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
    2.60 +        val rep_const = cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
    2.61          val cong' =
    2.62            Drule.export_without_context
    2.63              (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    2.64 @@ -259,7 +257,7 @@
    2.65            Drule.export_without_context
    2.66              (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    2.67          val (thy', defs', eqns', _) =
    2.68 -          fold ((make_constr_def tname T) (length constrs))
    2.69 +          fold (make_constr_def tname typedef T (length constrs))
    2.70              (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
    2.71        in
    2.72          (Sign.parent_path thy', defs', eqns @ [eqns'],
    2.73 @@ -268,7 +266,7 @@
    2.74  
    2.75      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) =
    2.76        fold dt_constr_defs
    2.77 -        (hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax)
    2.78 +        (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax)
    2.79          (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []);
    2.80  
    2.81  
    2.82 @@ -276,12 +274,11 @@
    2.83  
    2.84      val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
    2.85  
    2.86 -    val newT_iso_axms = map (fn (_, (_, td)) =>
    2.87 -      (collect_simp (#Abs_inverse td), #Rep_inverse td,
    2.88 -       collect_simp (#Rep td))) typedefs;
    2.89 +    val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) =>
    2.90 +      (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep));
    2.91  
    2.92 -    val newT_iso_inj_thms = map (fn (_, (_, td)) =>
    2.93 -      (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
    2.94 +    val newT_iso_inj_thms = typedefs |> map (fn (_, (_, {Abs_inject, Rep_inject, ...})) =>
    2.95 +      (collect_simp Abs_inject RS iffD1, Rep_inject RS iffD1));
    2.96  
    2.97      (********* isomorphisms between existing types and "unfolded" types *******)
    2.98  
    2.99 @@ -300,8 +297,7 @@
   2.100        let
   2.101          val argTs = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   2.102          val T = nth recTs k;
   2.103 -        val rep_name = nth all_rep_names k;
   2.104 -        val rep_const = Const (rep_name, T --> Univ_elT);
   2.105 +        val rep_const = Const (nth all_rep_names k, T --> Univ_elT);
   2.106          val constr = Const (cname, argTs ---> T);
   2.107  
   2.108          fun process_arg ks' dt (i2, i2', ts, Ts) =
   2.109 @@ -409,14 +405,14 @@
   2.110              val T = nth recTs i;
   2.111              val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
   2.112              val rep_set_name = nth rep_set_names i;
   2.113 -          in
   2.114 -            (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
   2.115 +            val concl1 =
   2.116 +              HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
   2.117                  HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $
   2.118 -                  HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)),
   2.119 -              Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i))
   2.120 -          end;
   2.121 +                  HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0));
   2.122 +            val concl2 = Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i);
   2.123 +          in (concl1, concl2) end;
   2.124  
   2.125 -        val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   2.126 +        val (ind_concl1, ind_concl2) = split_list (map mk_ind_concl ds);
   2.127  
   2.128          val rewrites = map mk_meta_eq iso_char_thms;
   2.129          val inj_thms' = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) inj_thms;
   2.130 @@ -592,28 +588,26 @@
   2.131        map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded;
   2.132      val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded;
   2.133  
   2.134 -    fun mk_indrule_lemma ((i, _), T) (prems, concls) =
   2.135 +    fun mk_indrule_lemma (i, _) T =
   2.136        let
   2.137 -        val Rep_t =
   2.138 -          Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i;
   2.139 -
   2.140 +        val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i;
   2.141          val Abs_t =
   2.142            if i < length newTs then
   2.143 -            Const (Sign.intern_const thy6 ("Abs_" ^ nth new_type_names i), Univ_elT --> T)
   2.144 -          else Const (@{const_name the_inv_into},
   2.145 +            Const (#Abs_name (#1 (#2 (nth typedefs i))), Univ_elT --> T)
   2.146 +          else
   2.147 +            Const (@{const_name the_inv_into},
   2.148                [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
   2.149              HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT);
   2.150 -      in
   2.151 -        (prems @
   2.152 -          [HOLogic.imp $
   2.153 +        val prem =
   2.154 +          HOLogic.imp $
   2.155              (Const (nth rep_set_names i, UnivT') $ Rep_t) $
   2.156 -              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   2.157 -         concls @
   2.158 -          [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i])
   2.159 -      end;
   2.160 +              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t));
   2.161 +        val concl =
   2.162 +          Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i;
   2.163 +      in (prem, concl) end;
   2.164  
   2.165      val (indrule_lemma_prems, indrule_lemma_concls) =
   2.166 -      fold mk_indrule_lemma (descr' ~~ recTs) ([], []);
   2.167 +      split_list (map2 mk_indrule_lemma descr' recTs);
   2.168  
   2.169      val cert = cterm_of thy6;
   2.170  
     3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Dec 14 20:36:17 2011 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Dec 14 21:54:32 2011 +0100
     3.3 @@ -16,13 +16,13 @@
     3.4        thm -> theory -> (string list * thm list) * theory
     3.5    val prove_case_thms : config -> string list -> descr list ->
     3.6      string list -> thm list -> theory -> (thm list list * string list) * theory
     3.7 -  val prove_split_thms : config -> string list -> descr list ->
     3.8 +  val prove_split_thms : config -> string list -> string list -> descr list ->
     3.9      thm list list -> thm list list -> thm list -> thm list list -> theory ->
    3.10      (thm * thm) list * theory
    3.11    val prove_nchotomys : config -> string list -> descr list ->
    3.12      thm list -> theory -> thm list * theory
    3.13 -  val prove_weak_case_congs : string list -> descr list -> theory -> thm list * theory
    3.14 -  val prove_case_congs : string list -> descr list ->
    3.15 +  val prove_weak_case_congs : string list -> string list -> descr list -> theory -> thm list * theory
    3.16 +  val prove_case_congs : string list -> string list -> descr list ->
    3.17      thm list -> thm list list -> theory -> thm list * theory
    3.18  end;
    3.19  
    3.20 @@ -262,7 +262,7 @@
    3.21               resolve_tac rec_unique_thms 1,
    3.22               resolve_tac rec_intrs 1,
    3.23               REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
    3.24 -       (Datatype_Prop.make_primrecs new_type_names descr thy2);
    3.25 +       (Datatype_Prop.make_primrecs reccomb_names descr thy2);
    3.26    in
    3.27      thy2
    3.28      |> Sign.add_path (space_implode "_" new_type_names)
    3.29 @@ -338,7 +338,7 @@
    3.30            Skip_Proof.prove_global thy2 [] [] t
    3.31              (fn _ =>
    3.32                EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
    3.33 -        (Datatype_Prop.make_cases new_type_names descr thy2);
    3.34 +        (Datatype_Prop.make_cases case_names descr thy2);
    3.35    in
    3.36      thy2
    3.37      |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
    3.38 @@ -351,7 +351,7 @@
    3.39  (******************************* case splitting *******************************)
    3.40  
    3.41  fun prove_split_thms (config : Datatype_Aux.config)
    3.42 -    new_type_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
    3.43 +    new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
    3.44    let
    3.45      val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
    3.46  
    3.47 @@ -374,10 +374,10 @@
    3.48  
    3.49      val split_thm_pairs =
    3.50        map prove_split_thms
    3.51 -        (Datatype_Prop.make_splits new_type_names descr thy ~~ constr_inject ~~
    3.52 +        (Datatype_Prop.make_splits case_names descr thy ~~ constr_inject ~~
    3.53            dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
    3.54  
    3.55 -    val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
    3.56 +    val (split_thms, split_asm_thms) = split_list split_thm_pairs
    3.57  
    3.58    in
    3.59      thy
    3.60 @@ -386,14 +386,14 @@
    3.61      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
    3.62    end;
    3.63  
    3.64 -fun prove_weak_case_congs new_type_names descr thy =
    3.65 +fun prove_weak_case_congs new_type_names case_names descr thy =
    3.66    let
    3.67      fun prove_weak_case_cong t =
    3.68       Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    3.69 -       (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]);
    3.70 +       (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
    3.71  
    3.72      val weak_case_congs =
    3.73 -      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr thy);
    3.74 +      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
    3.75  
    3.76    in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
    3.77  
    3.78 @@ -421,7 +421,7 @@
    3.79  
    3.80    in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
    3.81  
    3.82 -fun prove_case_congs new_type_names descr nchotomys case_thms thy =
    3.83 +fun prove_case_congs new_type_names case_names descr nchotomys case_thms thy =
    3.84    let
    3.85      fun prove_case_cong ((t, nchotomy), case_rewrites) =
    3.86        let
    3.87 @@ -444,8 +444,8 @@
    3.88        end;
    3.89  
    3.90      val case_congs =
    3.91 -      map prove_case_cong (Datatype_Prop.make_case_congs
    3.92 -        new_type_names descr thy ~~ nchotomys ~~ case_thms);
    3.93 +      map prove_case_cong
    3.94 +        (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms);
    3.95  
    3.96    in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
    3.97  
     4.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 14 20:36:17 2011 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 14 21:54:32 2011 +0100
     4.3 @@ -300,12 +300,13 @@
     4.4      val ((case_rewrites, case_names), thy6) = thy5
     4.5        |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites;
     4.6      val (case_congs, thy7) = thy6
     4.7 -      |> Datatype_Abs_Proofs.prove_case_congs new_type_names descr nchotomys case_rewrites;
     4.8 +      |> Datatype_Abs_Proofs.prove_case_congs new_type_names case_names descr
     4.9 +        nchotomys case_rewrites;
    4.10      val (weak_case_congs, thy8) = thy7
    4.11 -      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr;
    4.12 +      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names case_names descr;
    4.13      val (splits, thy9) = thy8
    4.14        |> Datatype_Abs_Proofs.prove_split_thms
    4.15 -        config new_type_names descr inject distinct exhaust case_rewrites;
    4.16 +        config new_type_names case_names descr inject distinct exhaust case_rewrites;
    4.17  
    4.18      val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
    4.19      val dt_infos = map_index
     5.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 14 20:36:17 2011 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 14 21:54:32 2011 +0100
     5.3 @@ -204,7 +204,7 @@
     5.4  
     5.5    in (rec_result_Ts, reccomb_fn_Ts) end;
     5.6  
     5.7 -fun make_primrecs new_type_names descr thy =
     5.8 +fun make_primrecs reccomb_names descr thy =
     5.9    let
    5.10      val descr' = flat descr;
    5.11      val recTs = Datatype_Aux.get_rec_types descr';
    5.12 @@ -216,11 +216,6 @@
    5.13        map (uncurry (Datatype_Aux.mk_Free "f"))
    5.14          (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
    5.15  
    5.16 -    val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
    5.17 -    val reccomb_names =
    5.18 -      map (Sign.intern_const thy)
    5.19 -        (if length descr' = 1 then [big_reccomb_name]
    5.20 -         else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr')));
    5.21      val reccombs =
    5.22        map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
    5.23          (reccomb_names ~~ recTs ~~ rec_result_Ts);
    5.24 @@ -256,7 +251,7 @@
    5.25  
    5.26  (****************** make terms of form  t_case f1 ... fn  *********************)
    5.27  
    5.28 -fun make_case_combs new_type_names descr thy fname =
    5.29 +fun make_case_combs case_names descr thy fname =
    5.30    let
    5.31      val descr' = flat descr;
    5.32      val recTs = Datatype_Aux.get_rec_types descr';
    5.33 @@ -268,8 +263,6 @@
    5.34        map (fn (_, cargs) =>
    5.35          let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs
    5.36          in Ts ---> T' end) constrs) (hd descr);
    5.37 -
    5.38 -    val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names;
    5.39    in
    5.40      map (fn ((name, Ts), T) => list_comb
    5.41        (Const (name, Ts @ [T] ---> T'),
    5.42 @@ -279,7 +272,7 @@
    5.43  
    5.44  (**************** characteristic equations for case combinator ****************)
    5.45  
    5.46 -fun make_cases new_type_names descr thy =
    5.47 +fun make_cases case_names descr thy =
    5.48    let
    5.49      val descr' = flat descr;
    5.50      val recTs = Datatype_Aux.get_rec_types descr';
    5.51 @@ -296,14 +289,14 @@
    5.52        end;
    5.53    in
    5.54      map (fn (((_, (_, _, constrs)), T), comb_t) =>
    5.55 -      map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
    5.56 -        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr thy "f"))
    5.57 +      map (make_case T comb_t) (constrs ~~ snd (strip_comb comb_t)))
    5.58 +        (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f")
    5.59    end;
    5.60  
    5.61  
    5.62  (*************************** the "split" - equations **************************)
    5.63  
    5.64 -fun make_splits new_type_names descr thy =
    5.65 +fun make_splits case_names descr thy =
    5.66    let
    5.67      val descr' = flat descr;
    5.68      val recTs = Datatype_Aux.get_rec_types descr';
    5.69 @@ -338,14 +331,14 @@
    5.70        end
    5.71  
    5.72    in
    5.73 -    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr thy "f")
    5.74 +    map make_split (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f")
    5.75    end;
    5.76  
    5.77  (************************* additional rules for TFL ***************************)
    5.78  
    5.79 -fun make_weak_case_congs new_type_names descr thy =
    5.80 +fun make_weak_case_congs case_names descr thy =
    5.81    let
    5.82 -    val case_combs = make_case_combs new_type_names descr thy "f";
    5.83 +    val case_combs = make_case_combs case_names descr thy "f";
    5.84  
    5.85      fun mk_case_cong comb =
    5.86        let
    5.87 @@ -372,10 +365,10 @@
    5.88   *      (ty_case f1..fn M = ty_case g1..gn M')
    5.89   *---------------------------------------------------------------------------*)
    5.90  
    5.91 -fun make_case_congs new_type_names descr thy =
    5.92 +fun make_case_congs case_names descr thy =
    5.93    let
    5.94 -    val case_combs = make_case_combs new_type_names descr thy "f";
    5.95 -    val case_combs' = make_case_combs new_type_names descr thy "g";
    5.96 +    val case_combs = make_case_combs case_names descr thy "f";
    5.97 +    val case_combs' = make_case_combs case_names descr thy "g";
    5.98  
    5.99      fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
   5.100        let
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 14 20:36:17 2011 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 14 21:54:32 2011 +0100
     6.3 @@ -903,9 +903,9 @@
     6.4  fun datatype_names_of_case_name thy case_name =
     6.5    map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
     6.6  
     6.7 -fun make_case_distribs new_type_names descr thy =
     6.8 +fun make_case_distribs case_names descr thy =
     6.9    let
    6.10 -    val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
    6.11 +    val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
    6.12      fun make comb =
    6.13        let
    6.14          val Type ("fun", [T, T']) = fastype_of comb;
    6.15 @@ -932,10 +932,10 @@
    6.16  
    6.17  fun case_rewrites thy Tcon =
    6.18    let
    6.19 -    val {descr, ...} = Datatype.the_info thy Tcon
    6.20 +    val {descr, case_name, ...} = Datatype.the_info thy Tcon
    6.21    in
    6.22      map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
    6.23 -      (make_case_distribs [Tcon] [descr] thy)
    6.24 +      (make_case_distribs [case_name] [descr] thy)
    6.25    end
    6.26  
    6.27  fun instantiated_case_rewrites thy Tcon =