Replaced xstring by thmref.

--- a/src/ZF/Tools/datatype_package.ML	Mon Jan 24 18:11:06 2005 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Mon Jan 24 18:12:22 2005 +0100
@@ -36,8 +36,8 @@
   val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
     thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
   val add_datatype: string * string list -> (string * string list * mixfix) list list ->
-    (xstring * Args.src list) list * (xstring * Args.src list) list *
-    (xstring * Args.src list) list -> theory -> theory * inductive_result * datatype_result
+    (thmref * Args.src list) list * (thmref * Args.src list) list *
+    (thmref * Args.src list) list -> theory -> theory * inductive_result * datatype_result
 end;
 
 functor Add_datatype_def_Fun

--- a/src/ZF/Tools/inductive_package.ML	Mon Jan 24 18:11:06 2005 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Jan 24 18:12:22 2005 +0100
@@ -35,8 +35,8 @@
     -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   val add_inductive: string list * string ->
     ((bstring * string) * Args.src list) list ->
-    (xstring * Args.src list) list * (xstring * Args.src list) list *
-    (xstring * Args.src list) list * (xstring * Args.src list) list ->
+    (thmref * Args.src list) list * (thmref * Args.src list) list *
+    (thmref * Args.src list) list * (thmref * Args.src list) list ->
     theory -> theory * inductive_result
 end;