Adapted to changes in interface of add_inductive_i.

--- a/src/HOL/Nominal/nominal_package.ML	Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Sep 28 10:32:38 2007 +0200
@@ -596,7 +596,7 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       setmp InductivePackage.quiet_mode false
         (InductivePackage.add_inductive_global false big_rep_name false true false
-           (map (fn (s, T) => (s, SOME (T --> HOLogic.boolT), NoSyn))
+           (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
               (rep_set_names' ~~ recTs'))
            [] (map (fn x => (("", []), x)) intr_ts) []) thy3;
 
@@ -1523,8 +1523,8 @@
       thy10 |>
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_global false big_rec_name false false false
-           (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
-           (map (apsnd SOME o dest_Free) rec_fns)
+           (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+           (map dest_Free rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) []) ||>
       PureThy.hide_thms true [NameSpace.append
         (Sign.full_name thy10 big_rec_name) "induct"];

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 10:32:38 2007 +0200
@@ -156,8 +156,8 @@
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_global false big_rec_name' false false true
-           (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
-           (map (apsnd SOME o dest_Free) rec_fns)
+           (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+           (map dest_Free rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 10:32:38 2007 +0200
@@ -178,7 +178,7 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       setmp InductivePackage.quiet_mode (! quiet_mode)
         (InductivePackage.add_inductive_global false big_rec_name false true false
-           (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
+           (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) []) thy1;
 
     (********************************* typedef ********************************)

--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Sep 28 10:32:38 2007 +0200
@@ -45,7 +45,7 @@
                                            false (* no coind *)
                                            false (* elims, please *)
                                            false (* induction thm please *)
-                                           [(R, SOME T, NoSyn)] (* the relation *)
+                                           [((R, T), NoSyn)] (* the relation *)
                                            [] (* no parameters *)
                                            (map (fn t => (("", []), t)) defs) (* the intros *)
                                            [] (* no special monos *)

--- a/src/HOL/Tools/inductive_realizer.ML	Fri Sep 28 10:30:51 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Sep 28 10:32:38 2007 +0200
@@ -340,10 +340,10 @@
             (Logic.strip_assums_concl rintr));
           val s' = Sign.base_name s;
           val T' = Logic.unvarifyT T
-        in ((s', SOME T', NoSyn),
+        in (((s', T'), NoSyn),
           (Const (s, T'), Free (s', T')))
         end) rintrs));
-    val rlzparams = map (fn Var ((s, _), T) => (s, SOME (Logic.unvarifyT T)))
+    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
       (List.take (snd (strip_comb
         (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));