1) have adjusted the swapping of the result type
in add_datatype_i
2) have replaced map_nth_elem by Library.nth_map
(there seems to be a clash with an existing
nth_map somewhere - therefore the "Library")

--- a/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 22:37:57 2005 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Oct 29 14:37:32 2005 +0200
@@ -1039,7 +1039,7 @@
     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
 
-    val (thy1, {induction, ...}) =
+    val ({induction, ...},thy1) =
       DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
 
     val SOME {descr, ...} = Symtab.lookup
@@ -1498,9 +1498,9 @@
     fun strip_suffix i s = implode (List.take (explode s, size s - i));
 
     (** strips the "_Rep" in type names *)
-    fun strip_nth_name i s =
-      let val xs = NameSpace.unpack s
-      in NameSpace.pack (map_nth_elem (length xs - i) (strip_suffix 4) xs) end;
+    fun strip_nth_name i s = 
+      let val xs = NameSpace.unpack s; 
+      in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val descr'' = List.mapPartial
       (fn (i, ("nominal.nOption", _, _)) => NONE
@@ -1511,6 +1511,7 @@
                 foldl (fn (dt, dts) =>
                   let val (dts', dt') = strip_option dt
                   in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr;
+
     val (descr1, descr2) = splitAt (length new_type_names, descr'');
     val descr' = [descr1, descr2];