# HG changeset patch
# User berghofe
# Date 1034252810 -7200
# Node ID 63d1790a43edceccce89ecc35808cae725085a86
# Parent  993576f4de3007954957f5f5b9722850e6508d8a
Reimplemented parts of datatype package dealing with datatypes involving
function types. Now also supports functions with more than one argument.

diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -18,31 +18,29 @@
 
 signature DATATYPE_ABS_PROOFS =
 sig
-  val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      thm -> theory attribute list -> theory -> theory * thm list
-  val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+  val prove_casedist_thms : string list ->
+    DatatypeAux.descr list -> (string * sort) list -> thm ->
+    theory attribute list -> theory -> theory * thm list
+  val prove_primrec_thms : bool -> string list ->
+    DatatypeAux.descr list -> (string * sort) list ->
       DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
         simpset -> thm -> theory -> theory * (string list * thm list)
-  val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+  val prove_case_thms : bool -> string list ->
+    DatatypeAux.descr list -> (string * sort) list ->
       string list -> thm list -> theory -> theory * (thm list list * string list)
-  val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+  val prove_split_thms : string list ->
+    DatatypeAux.descr list -> (string * sort) list ->
       thm list list -> thm list list -> thm list -> thm list list -> theory ->
         theory * (thm * thm) list
-  val prove_size_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+  val prove_size_thms : bool -> string list ->
+    DatatypeAux.descr list -> (string * sort) list ->
       string list -> thm list -> theory -> theory * thm list
-  val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      thm list -> theory -> theory * thm list
-  val prove_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> theory * thm list
-  val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+  val prove_nchotomys : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> thm list -> theory -> theory * thm list
+  val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> theory * thm list
+  val prove_case_congs : string list ->
+    DatatypeAux.descr list -> (string * sort) list ->
       thm list -> thm list list -> theory -> theory * thm list
 end;
 
@@ -51,10 +49,6 @@
 
 open DatatypeAux;
 
-val thin = read_instantiate_sg (Theory.sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
-
-val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
-
 (************************ case distinction theorems ***************************)
 
 fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
@@ -99,8 +93,6 @@
   let
     val _ = message "Constructing primrec combinators ...";
 
-    val fun_rel_comp_name = "Relation.fun_rel_comp";
-
     val big_name = space_implode "_" new_type_names;
     val thy0 = add_path flat_names big_name thy;
 
@@ -126,9 +118,8 @@
           val Ts = map (typ_of_dtyp descr' sorts) cargs;
           val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
 
-          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
-            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
-               T --> nth_elem (k, rec_result_Ts);
+          fun mk_argT (dt, T) =
+            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
 
           val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
@@ -148,20 +139,17 @@
       let
         fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
           let val free1 = mk_Free "x" U j
-          in (case (dt, U) of
-             (DtRec m, _) =>
-               let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
-               in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
-                 (HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
+          in (case (strip_dtyp dt, strip_type U) of
+             ((_, DtRec m), (Us, _)) =>
+               let
+                 val free2 = mk_Free "y" (Us ---> nth_elem (m, rec_result_Ts)) k;
+                 val i = length Us
+               in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
+                     (map (pair "x") Us, HOLogic.mk_mem (HOLogic.mk_prod
+                       (app_bnds free1 i, app_bnds free2 i),
+                         nth_elem (m, rec_sets)))) :: prems,
                    free1::t1s, free2::t2s)
                end
-           | (DtType ("fun", [_, DtRec m]), U' as Type ("fun", [T', _])) =>
-               let val free2 = mk_Free "y" (T' --> nth_elem (m, rec_result_Ts)) k
-               in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem (free2,
-                 Const (fun_rel_comp_name, [U', snd (strip_type (nth_elem (m, rec_set_Ts)))] --->
-                   HOLogic.mk_setT (T' --> nth_elem (m, rec_result_Ts))) $
-                     free1 $ nth_elem (m, rec_sets))))::prems, free1::t1s, free2::t2s)
-               end
            | _ => (j + 1, k, prems, free1::t1s, t2s))
           end;
 
@@ -180,7 +168,7 @@
     val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name' false false true
-           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono]) thy0;
+           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
@@ -202,16 +190,14 @@
             val k = length (filter is_rec_type cargs)
 
           in (EVERY [DETERM tac,
-                REPEAT (dtac fun_rel_comp_unique 1),
                 REPEAT (etac ex1E 1), rtac ex1I 1,
                 DEPTH_SOLVE_1 (ares_tac [intr] 1),
-                REPEAT_DETERM_N k (etac thin 1),
+                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
                 etac elim 1,
                 REPEAT_DETERM_N j distinct_tac,
                 etac Pair_inject 1, TRY (dresolve_tac inject 1),
                 REPEAT (etac conjE 1), hyp_subst_tac 1,
-                REPEAT (etac allE 1),
-                REPEAT (dtac mp 1 THEN atac 1),
+                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
                 TRY (hyp_subst_tac 1),
                 rtac refl 1,
                 REPEAT_DETERM_N (n - j - 1) distinct_tac],
@@ -236,7 +222,8 @@
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
         val (tac, _) = foldl mk_unique_tac
-          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1, rec_intrs),
+          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
+              THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
 
       in split_conj_thm (prove_goalw_cterm []
@@ -277,8 +264,7 @@
         [rtac the1_equality 1,
          resolve_tac rec_unique_thms 1,
          resolve_tac rec_intrs 1,
-         rewrite_goals_tac [o_def, fun_rel_comp_def],
-         REPEAT ((rtac CollectI 1 THEN rtac allI 1) ORELSE resolve_tac rec_total_thms 1)]))
+         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
            (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
 
   in
@@ -302,8 +288,7 @@
     val newTs = take (length (hd descr), recTs);
     val T' = TFree (variant used "'t", HOLogic.typeS);
 
-    fun mk_dummyT (DtRec _) = T'
-      | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
+    fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
 
     val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
       let
@@ -401,8 +386,9 @@
 (******************************* size functions *******************************)
 
 fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
-  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
-    (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) (flat descr)
+  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
+    is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
+      (flat descr)
   then
     (thy, [])
   else
diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -25,6 +25,9 @@
   val mk_conj : term list -> term
   val mk_disj : term list -> term
 
+  val app_bnds : term -> int -> term
+
+  val cong_tac : int -> tactic
   val indtac : thm -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
 
@@ -44,25 +47,21 @@
   val dtyp_of_typ : (string * string list) list -> typ -> dtyp
   val mk_Free : string -> typ -> int -> term
   val is_rec_type : dtyp -> bool
-  val typ_of_dtyp : (int * (string * dtyp list *
-    (string * dtyp list) list)) list -> (string * sort) list -> dtyp -> typ
+  val typ_of_dtyp : descr -> (string * sort) list -> dtyp -> typ
   val dest_DtTFree : dtyp -> string
   val dest_DtRec : dtyp -> int
+  val strip_dtyp : dtyp -> dtyp list * dtyp
+  val body_index : dtyp -> int
+  val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
   val dest_TFree : typ -> string
-  val get_nonrec_types : (int * (string * dtyp list *
-    (string * dtyp list) list)) list -> (string * sort) list -> typ list
-  val get_branching_types : (int * (string * dtyp list *
-    (string * dtyp list) list)) list -> (string * sort) list -> typ list
-  val get_rec_types : (int * (string * dtyp list *
-    (string * dtyp list) list)) list -> (string * sort) list -> typ list
-  val check_nonempty : (int * (string * dtyp list *
-    (string * dtyp list) list)) list list -> unit
+  val get_nonrec_types : descr -> (string * sort) list -> typ list
+  val get_branching_types : descr -> (string * sort) list -> typ list
+  val get_arities : descr -> int list
+  val get_rec_types : descr -> (string * sort) list -> typ list
+  val check_nonempty : descr list -> unit
   val unfold_datatypes : 
-    Sign.sg -> (int * (string * dtyp list * (string * dtyp list) list)) list ->
-      (string * sort) list -> datatype_info Symtab.table ->
-        (int * (string * dtyp list * (string * dtyp list) list)) list -> int ->
-          (int * (string * dtyp list *
-            (string * dtyp list) list)) list list * int
+    Sign.sg -> descr -> (string * sort) list -> datatype_info Symtab.table ->
+      descr -> int -> descr list * int
 end;
 
 structure DatatypeAux : DATATYPE_AUX =
@@ -105,6 +104,23 @@
 val mk_conj = foldr1 (HOLogic.mk_binop "op &");
 val mk_disj = foldr1 (HOLogic.mk_binop "op |");
 
+fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
+
+
+fun cong_tac i st = (case Logic.strip_assums_concl
+  (nth_elem (i - 1, prems_of st)) of
+    _ $ (_ $ (f $ x) $ (g $ y)) =>
+      let
+        val cong' = lift_rule (st, i) cong;
+        val _ $ (_ $ (f' $ x') $ (g' $ y')) =
+          Logic.strip_assums_concl (prop_of cong');
+        val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
+          apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
+            apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
+      in compose_tac (false, cterm_instantiate insts cong', 2) i st
+        handle THM _ => no_tac st
+      end
+  | _ => no_tac st);
 
 (* instantiate induction rule *)
 
@@ -198,6 +214,14 @@
   | is_rec_type (DtRec _) = true
   | is_rec_type _ = false;
 
+fun strip_dtyp (DtType ("fun", [T, U])) = apfst (cons T) (strip_dtyp U)
+  | strip_dtyp T = ([], T);
+
+val body_index = dest_DtRec o snd o strip_dtyp;
+
+fun mk_fun_dtyp [] U = U
+  | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
+
 fun dest_TFree (TFree (n, _)) = n;
 
 fun name_of_typ (Type (s, Ts)) = space_implode "_"
@@ -223,14 +247,9 @@
 (* find all non-recursive types in datatype description *)
 
 fun get_nonrec_types descr sorts =
-  let fun add (Ts, T as DtTFree _) = T ins Ts
-        | add (Ts, T as DtType ("fun", [_, DtRec _])) = Ts
-        | add (Ts, T as DtType _) = T ins Ts
-        | add (Ts, _) = Ts
-  in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+  map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
     foldl (fn (Ts', (_, cargs)) =>
-      foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
-  end;
+      filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
 
 (* get all recursive types in datatype description *)
 
@@ -239,13 +258,14 @@
 
 (* get all branching types *)
 
-fun get_branching_types descr sorts = 
-  let fun add (Ts, DtType ("fun", [T, DtRec _])) = T ins Ts
-        | add (Ts, _) = Ts
-  in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
-    foldl (fn (Ts', (_, cargs)) =>
-      foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
-  end;
+fun get_branching_types descr sorts =
+  map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+    foldl (fn (Ts', (_, cargs)) => foldr op union (map (fst o strip_dtyp)
+      cargs, Ts')) (Ts, constrs)) ([], descr));
+
+fun get_arities descr = foldl (fn (is, (_, (_, _, constrs))) =>
+  foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
+    (filter is_rec_type cargs) union is') (is, constrs)) ([], descr);
 
 (* nonemptiness check for datatypes *)
 
@@ -255,11 +275,10 @@
     fun is_nonempty_dt is i =
       let
         val (_, _, constrs) = the (assoc (descr', i));
-        fun arg_nonempty (DtRec i) = if i mem is then false
+        fun arg_nonempty (_, DtRec i) = if i mem is then false
               else is_nonempty_dt (i::is) i
-          | arg_nonempty (DtType ("fun", [_, T])) = arg_nonempty T
           | arg_nonempty _ = true;
-      in exists ((forall arg_nonempty) o snd) constrs
+      in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
       end
   in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
     (fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
@@ -290,22 +309,21 @@
 
     (* unfold a single constructor argument *)
 
-    fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
-          if is_rec_type T then
-            if tname = "fun" then
-              if is_rec_type (hd dts) then
-                typ_error T "Non-strictly positive recursive occurrence of type"
-              else
-                (case hd (tl dts) of
-                   DtType ("fun", _) => typ_error T "Curried function types not allowed"
-                 | T' => let val (i', [T''], descrs') = unfold_arg ((i, [], descrs), T')
-                         in (i', Ts @ [DtType (tname, [hd dts, T''])], descrs') end)
-            else
-              let val (index, descr) = get_dt_descr T i tname dts;
-                  val (descr', i') = unfold_datatypes sign orig_descr sorts dt_info descr (i + length descr)
-              in (i', Ts @ [DtRec index], descrs @ descr') end
-          else (i, Ts @ [T], descrs)
-      | unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
+    fun unfold_arg ((i, Ts, descrs), T) =
+      if is_rec_type T then
+        let val (Us, U) = strip_dtyp T
+        in if exists is_rec_type Us then
+            typ_error T "Non-strictly positive recursive occurrence of type"
+          else (case U of
+              DtType (tname, dts) =>  
+                let
+                  val (index, descr) = get_dt_descr T i tname dts;
+                  val (descr', i') = unfold_datatypes sign orig_descr sorts
+                    dt_info descr (i + length descr)
+                in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
+            | _ => (i, Ts @ [T], descrs))
+        end
+      else (i, Ts @ [T], descrs);
 
     (* unfold a constructor *)
 
diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -450,7 +450,8 @@
     val newTs = take (length (hd descr), recTs);
 
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
-      (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
+      (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
+        cargs) constrs) descr';
 
     (**** declare new types and constants ****)
 
@@ -470,9 +471,8 @@
           val Ts = map (typ_of_dtyp descr' sorts) cargs;
           val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
 
-          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
-            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
-               T --> nth_elem (k, rec_result_Ts);
+          fun mk_argT (dt, T) =
+            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
 
           val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -11,38 +11,27 @@
   val dtK : int ref
   val indexify_names: string list -> string list
   val make_tnames: typ list -> string list
-  val make_injs : (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      term list list
-  val make_ind : (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
-  val make_casedists : (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
-  val make_primrecs : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> term list
-  val make_cases : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> term list list
-  val make_distincts : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> term list list
-  val make_splits : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> (term * term) list
-  val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
-  val make_size : (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> term list
-  val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> term list
-  val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      theory -> term list
-  val make_nchotomys : (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
+  val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
+  val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
+  val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
+  val make_primrecs : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> term list
+  val make_cases : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> term list list
+  val make_distincts : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> term list list
+  val make_splits : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> (term * term) list
+  val make_case_trrules : string list -> DatatypeAux.descr list ->
+    ast Syntax.trrule list
+  val make_size : DatatypeAux.descr list -> (string * sort) list ->
+    theory -> term list
+  val make_weak_case_congs : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> term list
+  val make_case_congs : string list -> DatatypeAux.descr list ->
+    (string * sort) list -> theory -> term list
+  val make_nchotomys : DatatypeAux.descr list ->
+    (string * sort) list -> term list
 end;
 
 structure DatatypeProp : DATATYPE_PROP =
@@ -111,11 +100,11 @@
 
     fun make_ind_prem k T (cname, cargs) =
       let
-        fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
-              (make_pred k T $ Free (s, T))
-          | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
-              all T $ Abs ("x", T, HOLogic.mk_Trueprop
-                (make_pred k U $ (Free (s, T') $ Bound 0)));
+        fun mk_prem ((dt, s), T) =
+          let val (Us, U) = strip_type T
+          in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
+          end;
 
         val recs = filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
@@ -168,8 +157,6 @@
 
 fun make_primrecs new_type_names descr sorts thy =
   let
-    val o_name = "Fun.comp";
-
     val sign = Theory.sign_of thy;
 
     val descr' = flat descr;
@@ -185,9 +172,8 @@
           val Ts = map (typ_of_dtyp descr' sorts) cargs;
           val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
 
-          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
-            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
-               T --> nth_elem (k, rec_result_Ts);
+          fun mk_argT (dt, T) =
+            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
 
           val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
@@ -215,17 +201,17 @@
         val frees = map Free (tnames ~~ Ts);
         val frees' = map Free (rec_tnames ~~ recTs');
 
-        fun mk_reccomb (DtRec i, _) = nth_elem (i, reccombs)
-          | mk_reccomb (DtType ("fun", [_, DtRec i]), Type ("fun", [T, U])) =
-              let val T' = nth_elem (i, rec_result_Ts)
-              in Const (o_name, [U --> T', T --> U, T] ---> T') $ nth_elem (i, reccombs)
-              end;
+        fun mk_reccomb ((dt, T), t) =
+          let val (Us, U) = strip_type T
+          in list_abs (map (pair "x") Us,
+            nth_elem (body_index dt, reccombs) $ app_bnds t (length Us))
+          end;
 
-        val reccombs' = map mk_reccomb (recs ~~ recTs')
+        val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
 
       in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
         (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
-         list_comb (f, frees @ (map (op $) (reccombs' ~~ frees')))))], fs)
+         list_comb (f, frees @ reccombs')))], fs)
       end
 
   in fst (foldl (fn (x, ((dt, T), comb_t)) =>
diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -88,23 +88,18 @@
                 in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
                   (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
                 end
-            | mk_prems vs (((DtRec k, s), T) :: ds) = 
+            | mk_prems vs (((dt, s), T) :: ds) = 
                 let
+                  val k = body_index dt;
+                  val (Us, U) = strip_type T;
+                  val i = length Us;
                   val rT = nth_elem (k, rec_result_Ts);
-                  val r = Free ("r" ^ s, rT);
+                  val r = Free ("r" ^ s, Us ---> rT);
                   val (p, f) = mk_prems (vs @ [r]) ds
-                in (mk_all k ("r" ^ s) rT (Logic.mk_implies
-                  (HOLogic.mk_Trueprop (make_pred k rT T r (Free (s, T))), p)), f)
-                end
-            | mk_prems vs (((DtType ("fun", [_, DtRec k]), s),
-                  T' as Type ("fun", [T, U])) :: ds) =
-                let
-                  val rT = nth_elem (k, rec_result_Ts);
-                  val r = Free ("r" ^ s, T --> rT);
-                  val (p, f) = mk_prems (vs @ [r]) ds
-                in (mk_all k ("r" ^ s) (T --> rT) (Logic.mk_implies
-                  (all T $ Abs ("x", T, HOLogic.mk_Trueprop (make_pred k rT U
-                    (r $ Bound 0) (Free (s, T') $ Bound 0))), p)), f)
+                in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
+                  (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+                    (make_pred k rT U (app_bnds r i)
+                      (app_bnds (Free (s, T)) i))), p)), f)
                 end
 
         in (j + 1,
diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -15,11 +15,10 @@
 signature DATATYPE_REP_PROOFS =
 sig
   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
-    string list -> (int * (string * DatatypeAux.dtyp list *
-      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
-          -> theory -> theory * thm list list * thm list list * thm list list *
-            DatatypeAux.simproc_dist list * thm
+    string list -> DatatypeAux.descr list -> (string * sort) list ->
+      (string * mixfix) list -> (string * mixfix) list list -> theory attribute
+        -> theory -> theory * thm list list * thm list list * thm list list *
+          DatatypeAux.simproc_dist list * thm
 end;
 
 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -54,19 +53,15 @@
     val Leaf_name = "Datatype_Universe.Leaf";
     val Numb_name = "Datatype_Universe.Numb";
     val Lim_name = "Datatype_Universe.Lim";
-    val Funs_name = "Datatype_Universe.Funs";
-    val o_name = "Fun.comp";
-    val sum_case_name = "Datatype.sum.sum_case";
+    val Suml_name = "Datatype.Suml";
+    val Sumr_name = "Datatype.Sumr";
 
-    val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
-         In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
-         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
-        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
-         "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
-         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
-
-    val Funs_IntE = (Int_lower2 RS Funs_mono RS
-      (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
+    val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
+         In0_eq, In1_eq, In0_not_In1, In1_not_In0,
+         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
+        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
+         "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
+         "Lim_inject", "Suml_inject", "Sumr_inject"];
 
     val descr' = flat descr;
 
@@ -83,6 +78,7 @@
     val branchTs = get_branching_types descr' sorts;
     val branchT = if null branchTs then HOLogic.unitT
       else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
+    val arities = get_arities descr' \ 0;
     val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
     val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
     val recTs = get_rec_types descr' sorts;
@@ -131,16 +127,16 @@
           let
             val n2 = n div 2;
             val Type (_, [T1, T2]) = T;
-            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+            fun mkT U = (U --> Univ_elT) --> T --> Univ_elT
           in
-            if i <= n2 then
-              sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
-            else
-              sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
+            if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
+            else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
           end
       in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
       end;
 
+    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
+
     (************** generate introduction rules for representing set **********)
 
     val _ = message "Constructing representing sets ...";
@@ -149,28 +145,26 @@
 
     fun make_intr s n (i, (_, cargs)) =
       let
-        fun mk_prem (DtRec k, (j, prems, ts)) =
-              let val free_t = mk_Free "x" Univ_elT j
-              in (j + 1, (HOLogic.mk_mem (free_t,
-                Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
+        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
+            (dts, DtRec k) =>
+              let
+                val Ts = map (typ_of_dtyp descr' sorts) dts;
+                val free_t =
+                  app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
+              in (j + 1, list_all (map (pair "x") Ts,
+                  HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
+                    Const (nth_elem (k, rep_set_names), UnivT)))) :: prems,
+                mk_lim (Ts, free_t) :: ts)
               end
-          | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
-              let val T' = typ_of_dtyp descr' sorts T;
-                  val free_t = mk_Free "x" (T' --> Univ_elT) j
-              in (j + 1, (HOLogic.mk_mem (free_t,
-                Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
-                  Const (nth_elem (k, rep_set_names), UnivT)))::prems,
-                    Lim $ mk_fun_inj T' free_t::ts)
-              end
-          | mk_prem (dt, (j, prems, ts)) =
+          | _ =>
               let val T = typ_of_dtyp descr' sorts dt
               in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
-              end;
+              end);
 
         val (_, prems, ts) = foldr mk_prem (cargs, (1, [], []));
         val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
           (mk_univ_inj ts n i, Const (s, UnivT)))
-      in Logic.list_implies (map HOLogic.mk_Trueprop prems, concl)
+      in Logic.list_implies (prems, concl)
       end;
 
     val consts = map (fn s => Const (s, UnivT)) rep_set_names;
@@ -182,7 +176,7 @@
     val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name false true false
-           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1;
+           consts (map (fn x => (("", x), [])) intr_ts) []) thy1;
 
     (********************************* typedef ********************************)
 
@@ -191,7 +185,7 @@
         (TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None
           (rtac exI 1 THEN
             QUIET_BREADTH_FIRST (has_fewer_prems 1)
-            (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
+            (resolve_tac rep_intrs 1))) thy |> #1)
               (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
                 (take (length newTs, consts)) ~~ new_type_names));
 
@@ -216,16 +210,10 @@
         fun constr_arg (dt, (j, l_args, r_args)) =
           let val T = typ_of_dtyp descr' sorts dt;
               val free_t = mk_Free "x" T j
-          in (case dt of
-              DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
-                T --> Univ_elT) $ free_t)::r_args)
-            | DtType ("fun", [T', DtRec m]) =>
-                let val ([T''], T''') = strip_type T
-                in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
-                  (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
-                    Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
-                end
-
+          in (case (strip_dtyp dt, strip_type T) of
+              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
+                Const (nth_elem (m, all_rep_names), U --> Univ_elT) $
+                  app_bnds free_t (length Us)) :: r_args)
             | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
           end;
 
@@ -321,11 +309,11 @@
     (* isomorphisms are defined using primrec-combinators:                 *)
     (* generate appropriate functions for instantiating primrec-combinator *)
     (*                                                                     *)
-    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 ((Leaf h) $ y))        *)
+    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y))    *)
     (*                                                                     *)
     (* also generate characteristic equations for isomorphisms             *)
     (*                                                                     *)
-    (*   e.g.  dt_Rep_i (cons h t) = In1 ((dt_Rep_j h) $ (dt_Rep_i t))     *)
+    (*   e.g.  dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
     (*---------------------------------------------------------------------*)
 
     fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
@@ -337,24 +325,18 @@
         val constr = Const (cname, argTs ---> T);
 
         fun process_arg ks' ((i2, i2', ts, Ts), dt) =
-          let val T' = typ_of_dtyp descr' sorts dt
-          in (case dt of
-              DtRec j => if j mem ks' then
-                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
+          let
+            val T' = typ_of_dtyp descr' sorts dt;
+            val (Us, U) = strip_type T'
+          in (case strip_dtyp dt of
+              (_, DtRec j) => if j mem ks' then
+                  (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
+                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
+                   Ts @ [Us ---> Univ_elT])
                 else
-                  (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
-                    T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
-            | (DtType ("fun", [_, DtRec j])) =>
-                let val ([T''], T''') = strip_type T'
-                in if j mem ks' then
-                    (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
-                      (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
-                  else
-                    (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
-                      (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
-                        Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
-                          mk_Free "x" T' i2)], Ts)
-                end
+                  (i2 + 1, i2', ts @ [mk_lim (Us,
+                     Const (nth_elem (j, all_rep_names), U --> Univ_elT) $
+                       app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
             | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
           end;
 
@@ -406,18 +388,25 @@
 
     fun mk_funs_inv thm =
       let
-        val [_, t] = prems_of Funs_inv;
-        val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
-        val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
-        val [_ $ (_ $ _ $ R')] = prems_of thm;
-        val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
-        val inv' = cterm_instantiate (map 
-          ((pairself (cterm_of (sign_of_thm thm))) o
-           (apsnd (map_term_types (incr_tvar 1))))
-             [(R, R'), (r, r'), (a, a')]) Funs_inv
-      in
-        rule_by_tactic (atac 2) (thm RSN (2, inv'))
-      end;
+        val {sign, prop, ...} = rep_thm thm;
+        val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
+          (_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop;
+        val used = add_term_tfree_names (a, []);
+
+        fun mk_thm i =
+          let
+            val Ts = map (TFree o rpair HOLogic.typeS)
+              (variantlist (replicate i "'t", used));
+            val f = Free ("f", Ts ---> U)
+          in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
+            (HOLogic.mk_Trueprop (HOLogic.list_all
+               (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
+             HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
+               r $ (a $ app_bnds f i)), f))))) (fn prems =>
+                 [cut_facts_tac prems 1, REPEAT (rtac ext 1),
+                  REPEAT (etac allE 1), rtac thm 1, atac 1])
+          end
+      in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
 
     (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
 
@@ -440,8 +429,8 @@
         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
 
         val rewrites = map mk_meta_eq iso_char_thms;
-        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
-          (map snd newT_iso_inj_thms @ inj_thms));
+        val inj_thms' = map (fn r => r RS injD)
+          (map snd newT_iso_inj_thms @ inj_thms);
 
         val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
@@ -455,13 +444,15 @@
                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
                    (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
                    ORELSE (EVERY
-                     [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
-                        map make_elim (inj_thms' @
-                          [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
-                      REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
-                              (dtac inj_fun_lemma 1 THEN atac 1)),
-                      REPEAT (hyp_subst_tac 1),
-                      rtac refl 1])])])]);
+                     [REPEAT (eresolve_tac (Scons_inject ::
+                        map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
+                      REPEAT (cong_tac 1), rtac refl 1,
+                      REPEAT (atac 1 ORELSE (EVERY
+                        [REPEAT (rtac ext 1),
+                         REPEAT (eresolve_tac (mp :: allE ::
+                           map make_elim (Suml_inject :: Sumr_inject ::
+                             Lim_inject :: fun_cong :: inj_thms')) 1),
+                         atac 1]))])])])]);
 
         val inj_thms'' = map (fn r => r RS datatype_injI)
                              (split_conj_thm inj_thm);
@@ -472,11 +463,9 @@
 	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
 	      (fn _ =>
 	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
-		rewrite_goals_tac (o_def :: rewrites),
-		REPEAT (EVERY
-			[resolve_tac rep_intrs 1,
-			 REPEAT (FIRST [atac 1, etac spec 1,
-				 resolve_tac (FunsI :: elem_thms) 1])])]);
+		rewrite_goals_tac rewrites,
+		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
+                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
 
       in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
       end;
@@ -502,18 +491,20 @@
 
     (* all the theorems are proved by one single simultaneous induction *)
 
+    val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
+      iso_inj_thms_unfolded;
+
     val iso_thms = if length descr = 1 then [] else
       drop (length newTs, split_conj_thm
         (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
-           [indtac rep_induct 1,
+           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
             REPEAT (rtac TrueI 1),
+            rewrite_goals_tac (mk_meta_eq choice_eq ::
+              symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
+            rewrite_goals_tac (map symmetric range_eqs),
             REPEAT (EVERY
-              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
-               REPEAT (etac Funs_IntE 1),
-               REPEAT (eresolve_tac (rangeE ::
-                 map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1),
-               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
-                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
+              [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
+                 flat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
                TRY (hyp_subst_tac 1),
                rtac (sym RS range_eqI) 1,
                resolve_tac iso_char_thms 1])])));
@@ -523,8 +514,7 @@
       map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
         (iso_inj_thms_unfolded, iso_thms);
 
-    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
-      map mk_funs_inv Abs_inverse_thms');
+    val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms');
 
     (******************* freeness theorems for constructors *******************)
 
@@ -541,7 +531,7 @@
          rewrite_goals_tac rewrites,
          rtac refl 1,
          resolve_tac rep_intrs 2,
-         REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
+         REPEAT (resolve_tac iso_elem_thms 1)])
       end;
 
     (*--------------------------------------------------------------*)
@@ -575,17 +565,19 @@
     (* prove injectivity of constructors *)
 
     fun prove_constr_inj_thm rep_thms t =
-      let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
+      let val inj_thms = Scons_inject :: (map make_elim
         ((map (fn r => r RS injD) iso_inj_thms) @
-          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
+          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
+           Lim_inject, Suml_inject, Sumr_inject]))
       in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
         [rtac iffI 1,
          REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
          dresolve_tac rep_congs 1, dtac box_equals 1,
-         REPEAT (resolve_tac rep_thms 1), rewtac o_def,
+         REPEAT (resolve_tac rep_thms 1),
          REPEAT (eresolve_tac inj_thms 1),
-         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
-                  eresolve_tac inj_thms 1, atac 1]))])
+         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
+           REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
+           atac 1]))])
       end;
 
     val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
@@ -641,12 +633,12 @@
 
     val dt_induct = prove_goalw_cterm [] (cert
       (DatatypeProp.make_ind descr sorts)) (fn prems =>
-        [rtac indrule_lemma' 1, indtac rep_induct 1,
+        [rtac indrule_lemma' 1,
+         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
-           [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
+           [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
-            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
-              dtac FunsD 1, etac CollectD 1]))]))
+            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
     val (thy7, [dt_induct']) = thy6 |>
diff -r 993576f4de30 -r 63d1790a43ed src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -141,16 +141,13 @@
               (fnames', fnss', (Const ("arbitrary", dummyT))::fns))
         | Some (ls, cargs', rs, rhs, eq) =>
             let
-              fun rec_index (DtRec k) = k
-                | rec_index (DtType ("fun", [_, DtRec k])) = k;
-
               val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
               val rargs = map fst recs;
               val subs = map (rpair dummyT o fst) 
 		             (rev (rename_wrt_term rhs rargs));
               val ((fnames'', fnss''), rhs') = 
 		  (subst (map (fn ((x, y), z) =>
-			       (Free x, (rec_index y, Free z)))
+			       (Free x, (body_index y, Free z)))
 			  (recs ~~ subs))
 		   ((fnames', fnss'), rhs))
                   handle RecError s => primrec_eq_err sign s eq
@@ -257,7 +254,7 @@
       (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
        else primrec_err ("functions " ^ commas_quote names2 ^
          "\nare not mutually recursive"));
-    val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms';
+    val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
     val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
     val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
         (fn _ => [rtac refl 1])) eqns;