# HG changeset patch
# User wenzelm
# Date 938026703 -7200
# Node ID aa87cf5a15f5ec14bed54dabf0d925b14244a67d
# Parent  6e6dafacbc28bc864592f50b6dc2828a625d945e
ml_store_thm: no warning for "";

diff -r 6e6dafacbc28 -r aa87cf5a15f5 src/Pure/Thy/thm_database.ML
--- 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) =