# HG changeset patch
# User paulson
# Date 1115033436 -7200
# Node ID 9cb0a8ffa40da508ede1004ba43d3d0ecfe4ebbe
# Parent  0a4cc9b113c7a68801a3eb5f376306fa3010a184
fixed reference to top-level

diff -r 0a4cc9b113c7 -r 9cb0a8ffa40d src/HOL/thy_syntax.ML
--- 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