fixed reference to top-level
authorpaulson
Mon, 02 May 2005 13:30:36 +0200
changeset 15906 9cb0a8ffa40d
parent 15905 0a4cc9b113c7
child 15907 f377ba412dba
fixed reference to top-level
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