avoid fragile Sign.intern_const -- pass internal names directly;
tuned;

--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 20:36:17 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 21:54:32 2011 +0100
@@ -2045,7 +2045,7 @@
              resolve_tac rec_intrs 1,
              REPEAT (solve (prems @ rec_total_thms) prems 1)])
       end) (rec_eq_prems ~~
-        Datatype_Prop.make_primrecs new_type_names descr' thy12);
+        Datatype_Prop.make_primrecs reccomb_names descr' thy12);
 
     val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms)
       (descr1 ~~ distinct_thms ~~ inject_thms);

--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 20:36:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 21:54:32 2011 +0100
@@ -199,10 +199,9 @@
     (*********************** definition of constructors ***********************)
 
     val big_rep_name = big_name ^ "_Rep_";
-    val rep_names = map (prefix "Rep_") new_type_names;
     val rep_names' = map (fn i => big_rep_name ^ string_of_int i) (1 upto length (flat (tl descr)));
     val all_rep_names =
-      map (Sign.intern_const thy3) rep_names @
+      map (#Rep_name o #1 o #2) typedefs @
       map (Sign.full_bname thy3) rep_names';
 
     (* isomorphism declarations *)
@@ -212,7 +211,8 @@
 
     (* constructor definitions *)
 
-    fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
+    fun make_constr_def tname (typedef: Typedef.info) T n
+        ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
       let
         fun constr_arg dt (j, l_args, r_args) =
           let
@@ -224,19 +224,18 @@
                 (j + 1, free_t :: l_args, mk_lim
                   (Const (nth all_rep_names m, U --> Univ_elT) $
                     Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
-            | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
+            | _ => (j + 1, free_t :: l_args, (Leaf $ mk_inj T free_t) :: r_args))
           end;
 
         val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
         val constrT = map (Datatype_Aux.typ_of_dtyp descr') cargs ---> T;
-        val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
-        val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
+        val ({Abs_name, Rep_name, ...}, _) = typedef;
         val lhs = list_comb (Const (cname, constrT), l_args);
         val rhs = mk_univ_inj r_args n i;
-        val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
+        val def = Logic.mk_equals (lhs, Const (Abs_name, Univ_elT --> T) $ rhs);
         val def_name = Long_Name.base_name cname ^ "_def";
         val eqn =
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
+          HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
         val ([def_thm], thy') =
           thy
           |> Sign.add_consts_i [(cname', constrT, mx)]
@@ -246,12 +245,11 @@
 
     (* constructor definitions for datatype *)
 
-    fun dt_constr_defs ((((_, (_, _, constrs)), tname), T), constr_syntax)
+    fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax)
         (thy, defs, eqns, rep_congs, dist_lemmas) =
       let
         val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
-        val rep_const =
-          cterm_of thy (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
+        val rep_const = cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
         val cong' =
           Drule.export_without_context
             (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
@@ -259,7 +257,7 @@
           Drule.export_without_context
             (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns', _) =
-          fold ((make_constr_def tname T) (length constrs))
+          fold (make_constr_def tname typedef T (length constrs))
             (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
       in
         (Sign.parent_path thy', defs', eqns @ [eqns'],
@@ -268,7 +266,7 @@
 
     val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) =
       fold dt_constr_defs
-        (hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax)
+        (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax)
         (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []);
 
 
@@ -276,12 +274,11 @@
 
     val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
 
-    val newT_iso_axms = map (fn (_, (_, td)) =>
-      (collect_simp (#Abs_inverse td), #Rep_inverse td,
-       collect_simp (#Rep td))) typedefs;
+    val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) =>
+      (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep));
 
-    val newT_iso_inj_thms = map (fn (_, (_, td)) =>
-      (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
+    val newT_iso_inj_thms = typedefs |> map (fn (_, (_, {Abs_inject, Rep_inject, ...})) =>
+      (collect_simp Abs_inject RS iffD1, Rep_inject RS iffD1));
 
     (********* isomorphisms between existing types and "unfolded" types *******)
 
@@ -300,8 +297,7 @@
       let
         val argTs = map (Datatype_Aux.typ_of_dtyp descr') cargs;
         val T = nth recTs k;
-        val rep_name = nth all_rep_names k;
-        val rep_const = Const (rep_name, T --> Univ_elT);
+        val rep_const = Const (nth all_rep_names k, T --> Univ_elT);
         val constr = Const (cname, argTs ---> T);
 
         fun process_arg ks' dt (i2, i2', ts, Ts) =
@@ -409,14 +405,14 @@
             val T = nth recTs i;
             val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
             val rep_set_name = nth rep_set_names i;
-          in
-            (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
+            val concl1 =
+              HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
                 HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $
-                  HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)),
-              Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i))
-          end;
+                  HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0));
+            val concl2 = Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i);
+          in (concl1, concl2) end;
 
-        val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
+        val (ind_concl1, ind_concl2) = split_list (map mk_ind_concl ds);
 
         val rewrites = map mk_meta_eq iso_char_thms;
         val inj_thms' = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) inj_thms;
@@ -592,28 +588,26 @@
       map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded;
     val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded;
 
-    fun mk_indrule_lemma ((i, _), T) (prems, concls) =
+    fun mk_indrule_lemma (i, _) T =
       let
-        val Rep_t =
-          Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i;
-
+        val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i;
         val Abs_t =
           if i < length newTs then
-            Const (Sign.intern_const thy6 ("Abs_" ^ nth new_type_names i), Univ_elT --> T)
-          else Const (@{const_name the_inv_into},
+            Const (#Abs_name (#1 (#2 (nth typedefs i))), Univ_elT --> T)
+          else
+            Const (@{const_name the_inv_into},
               [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
             HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT);
-      in
-        (prems @
-          [HOLogic.imp $
+        val prem =
+          HOLogic.imp $
             (Const (nth rep_set_names i, UnivT') $ Rep_t) $
-              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
-         concls @
-          [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i])
-      end;
+              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t));
+        val concl =
+          Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i;
+      in (prem, concl) end;
 
     val (indrule_lemma_prems, indrule_lemma_concls) =
-      fold mk_indrule_lemma (descr' ~~ recTs) ([], []);
+      split_list (map2 mk_indrule_lemma descr' recTs);
 
     val cert = cterm_of thy6;
 

--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Dec 14 20:36:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Dec 14 21:54:32 2011 +0100
@@ -16,13 +16,13 @@
       thm -> theory -> (string list * thm list) * theory
   val prove_case_thms : config -> string list -> descr list ->
     string list -> thm list -> theory -> (thm list list * string list) * theory
-  val prove_split_thms : config -> string list -> descr list ->
+  val prove_split_thms : config -> string list -> string list -> descr list ->
     thm list list -> thm list list -> thm list -> thm list list -> theory ->
     (thm * thm) list * theory
   val prove_nchotomys : config -> string list -> descr list ->
     thm list -> theory -> thm list * theory
-  val prove_weak_case_congs : string list -> descr list -> theory -> thm list * theory
-  val prove_case_congs : string list -> descr list ->
+  val prove_weak_case_congs : string list -> string list -> descr list -> theory -> thm list * theory
+  val prove_case_congs : string list -> string list -> descr list ->
     thm list -> thm list list -> theory -> thm list * theory
 end;
 
@@ -262,7 +262,7 @@
              resolve_tac rec_unique_thms 1,
              resolve_tac rec_intrs 1,
              REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
-       (Datatype_Prop.make_primrecs new_type_names descr thy2);
+       (Datatype_Prop.make_primrecs reccomb_names descr thy2);
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
@@ -338,7 +338,7 @@
           Skip_Proof.prove_global thy2 [] [] t
             (fn _ =>
               EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
-        (Datatype_Prop.make_cases new_type_names descr thy2);
+        (Datatype_Prop.make_cases case_names descr thy2);
   in
     thy2
     |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
@@ -351,7 +351,7 @@
 (******************************* case splitting *******************************)
 
 fun prove_split_thms (config : Datatype_Aux.config)
-    new_type_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
+    new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
   let
     val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
 
@@ -374,10 +374,10 @@
 
     val split_thm_pairs =
       map prove_split_thms
-        (Datatype_Prop.make_splits new_type_names descr thy ~~ constr_inject ~~
+        (Datatype_Prop.make_splits case_names descr thy ~~ constr_inject ~~
           dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
 
-    val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
+    val (split_thms, split_asm_thms) = split_list split_thm_pairs
 
   in
     thy
@@ -386,14 +386,14 @@
     |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   end;
 
-fun prove_weak_case_congs new_type_names descr thy =
+fun prove_weak_case_congs new_type_names case_names descr thy =
   let
     fun prove_weak_case_cong t =
      Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
-       (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]);
+       (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
 
     val weak_case_congs =
-      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr thy);
+      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
 
   in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
 
@@ -421,7 +421,7 @@
 
   in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
 
-fun prove_case_congs new_type_names descr nchotomys case_thms thy =
+fun prove_case_congs new_type_names case_names descr nchotomys case_thms thy =
   let
     fun prove_case_cong ((t, nchotomy), case_rewrites) =
       let
@@ -444,8 +444,8 @@
       end;
 
     val case_congs =
-      map prove_case_cong (Datatype_Prop.make_case_congs
-        new_type_names descr thy ~~ nchotomys ~~ case_thms);
+      map prove_case_cong
+        (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms);
 
   in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
 

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 14 20:36:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 14 21:54:32 2011 +0100
@@ -300,12 +300,13 @@
     val ((case_rewrites, case_names), thy6) = thy5
       |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites;
     val (case_congs, thy7) = thy6
-      |> Datatype_Abs_Proofs.prove_case_congs new_type_names descr nchotomys case_rewrites;
+      |> Datatype_Abs_Proofs.prove_case_congs new_type_names case_names descr
+        nchotomys case_rewrites;
     val (weak_case_congs, thy8) = thy7
-      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr;
+      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names case_names descr;
     val (splits, thy9) = thy8
       |> Datatype_Abs_Proofs.prove_split_thms
-        config new_type_names descr inject distinct exhaust case_rewrites;
+        config new_type_names case_names descr inject distinct exhaust case_rewrites;
 
     val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
     val dt_infos = map_index

--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 14 20:36:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 14 21:54:32 2011 +0100
@@ -204,7 +204,7 @@
 
   in (rec_result_Ts, reccomb_fn_Ts) end;
 
-fun make_primrecs new_type_names descr thy =
+fun make_primrecs reccomb_names descr thy =
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr';
@@ -216,11 +216,6 @@
       map (uncurry (Datatype_Aux.mk_Free "f"))
         (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
 
-    val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
-    val reccomb_names =
-      map (Sign.intern_const thy)
-        (if length descr' = 1 then [big_reccomb_name]
-         else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr')));
     val reccombs =
       map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
         (reccomb_names ~~ recTs ~~ rec_result_Ts);
@@ -256,7 +251,7 @@
 
 (****************** make terms of form  t_case f1 ... fn  *********************)
 
-fun make_case_combs new_type_names descr thy fname =
+fun make_case_combs case_names descr thy fname =
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr';
@@ -268,8 +263,6 @@
       map (fn (_, cargs) =>
         let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs
         in Ts ---> T' end) constrs) (hd descr);
-
-    val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names;
   in
     map (fn ((name, Ts), T) => list_comb
       (Const (name, Ts @ [T] ---> T'),
@@ -279,7 +272,7 @@
 
 (**************** characteristic equations for case combinator ****************)
 
-fun make_cases new_type_names descr thy =
+fun make_cases case_names descr thy =
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr';
@@ -296,14 +289,14 @@
       end;
   in
     map (fn (((_, (_, _, constrs)), T), comb_t) =>
-      map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
-        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr thy "f"))
+      map (make_case T comb_t) (constrs ~~ snd (strip_comb comb_t)))
+        (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f")
   end;
 
 
 (*************************** the "split" - equations **************************)
 
-fun make_splits new_type_names descr thy =
+fun make_splits case_names descr thy =
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr';
@@ -338,14 +331,14 @@
       end
 
   in
-    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr thy "f")
+    map make_split (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f")
   end;
 
 (************************* additional rules for TFL ***************************)
 
-fun make_weak_case_congs new_type_names descr thy =
+fun make_weak_case_congs case_names descr thy =
   let
-    val case_combs = make_case_combs new_type_names descr thy "f";
+    val case_combs = make_case_combs case_names descr thy "f";
 
     fun mk_case_cong comb =
       let
@@ -372,10 +365,10 @@
  *      (ty_case f1..fn M = ty_case g1..gn M')
  *---------------------------------------------------------------------------*)
 
-fun make_case_congs new_type_names descr thy =
+fun make_case_congs case_names descr thy =
   let
-    val case_combs = make_case_combs new_type_names descr thy "f";
-    val case_combs' = make_case_combs new_type_names descr thy "g";
+    val case_combs = make_case_combs case_names descr thy "f";
+    val case_combs' = make_case_combs case_names descr thy "g";
 
     fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
       let

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 14 20:36:17 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 14 21:54:32 2011 +0100
@@ -903,9 +903,9 @@
 fun datatype_names_of_case_name thy case_name =
   map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
 
-fun make_case_distribs new_type_names descr thy =
+fun make_case_distribs case_names descr thy =
   let
-    val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
+    val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
     fun make comb =
       let
         val Type ("fun", [T, T']) = fastype_of comb;
@@ -932,10 +932,10 @@
 
 fun case_rewrites thy Tcon =
   let
-    val {descr, ...} = Datatype.the_info thy Tcon
+    val {descr, case_name, ...} = Datatype.the_info thy Tcon
   in
     map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
-      (make_case_distribs [Tcon] [descr] thy)
+      (make_case_distribs [case_name] [descr] thy)
   end
 
 fun instantiated_case_rewrites thy Tcon =