diff -r d3512dedbaea -r 05416ba8eef2 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Mon Jul 21 08:52:06 2003 +0200
+++ b/src/HOL/Tools/specification_package.ML	Mon Jul 21 08:53:56 2003 +0200
@@ -9,9 +9,9 @@
 signature SPECIFICATION_PACKAGE =
 sig
     val quiet_mode: bool ref
-    val add_specification: (bstring * bstring * bool) list -> bstring * Args.src list
+    val add_specification: (bstring * xstring * bool) list -> bstring * Args.src list
 			   -> theory * thm -> theory * thm
-    val add_specification_i: (bstring * bstring * bool) list -> bstring * theory attribute list
+    val add_specification_i: (bstring * xstring * bool) list -> bstring * theory attribute list
 			     -> theory * thm -> theory * thm
 end