# HG changeset patch
# User skalberg
# Date 1058770436 -7200
# Node ID 05416ba8eef24aa7b2a7c14035821ffb76219ac1
# Parent  d3512dedbaea98aab2fe4a91c7d67fb8d9197c2e
Changed bstring argument to xstring.

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