author | paulson |
Mon, 02 May 2005 13:30:36 +0200 | |
changeset 15906 | 9cb0a8ffa40d |
parent 15905 | 0a4cc9b113c7 |
child 15907 | f377ba412dba |
--- 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