fixed type of thms_containing;
authorwenzelm
Wed, 26 Nov 1997 16:37:43 +0100
changeset 4287 227a9e786c35
parent 4286 a09e3e6da2de
child 4288 3f5e8c4aa84d
fixed type of thms_containing;
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