Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ml_store_thm: no warning for "";
authorwenzelm
Wed, 22 Sep 1999 20:58:23 +0200
changeset 7573 aa87cf5a15f5
parent 7572 6e6dafacbc28
child 7574 5bcb7fc31caa
ml_store_thm: no warning for "";
src/Pure/Thy/thm_database.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/thm_database.ML	Wed Sep 22 20:57:51 1999 +0200
+++ b/src/Pure/Thy/thm_database.ML	Wed Sep 22 20:58:23 1999 +0200
@@ -64,6 +64,7 @@
 
 fun warn_ml name =
   if is_ml_identifier name then false
+  else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
 fun ml_store_thm (name, thm) =
isabelle