--- a/src/HOL/thy_syntax.ML	Mon May 02 11:03:27 2005 +0200
+++ b/src/HOL/thy_syntax.ML	Mon May 02 13:30:36 2005 +0200
@@ -94,7 +94,7 @@
   (*** and bindig theorems to ML identifiers    ***)
 
   fun mk_bind_thms_string names =
-   (case find_first (not o ThmDatabase.is_ml_identifier) names of
+   (case Library.find_first (not o ThmDatabase.is_ml_identifier) names of
       SOME id => (warning (id ^ " is not a valid identifier"); "")
     | NONE =>
         let