| changeset 7573 | aa87cf5a15f5 |
| parent 7446 | f43d3670a3cd |
| child 7609 | 1acbed762fc6 |
--- 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) =