# HG changeset patch
# User berghofe
# Date 1106586742 -3600
# Node ID d5d295a531b5e9da7b4b7c4269a58084c7ea0249
# Parent  dd48bf51aff196f2c98db9a235ad73375dda3841
Replaced xstring by thmref.

diff -r dd48bf51aff1 -r d5d295a531b5 src/ZF/Tools/datatype_package.ML
--- 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
diff -r dd48bf51aff1 -r d5d295a531b5 src/ZF/Tools/inductive_package.ML
--- 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;