# HG changeset patch
# User wenzelm
# Date 880558663 -3600
# Node ID 227a9e786c35721408a9d48a8a422b81644cec20
# Parent  a09e3e6da2de26b67dc5aa894c2451d003877a76
fixed type of thms_containing;

diff -r a09e3e6da2de -r 227a9e786c35 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Nov 26 16:37:17 1997 +0100
+++ b/src/Pure/Thy/thm_database.ML	Wed Nov 26 16:37:43 1997 +0100
@@ -14,7 +14,7 @@
   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
   val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit
   (*these peek at the proof state!*)
-  val thms_containing: string list -> (string * thm) list
+  val thms_containing: xstring list -> (string * thm) list
   val findI: int -> (string * thm) list
   val findEs: int -> (string * thm) list
   val findE: int -> int -> (string * thm) list