equal
deleted
inserted
replaced
62 fun is_ml_identifier name = |
62 fun is_ml_identifier name = |
63 Syntax.is_identifier name andalso not (name mem ml_reserved); |
63 Syntax.is_identifier name andalso not (name mem ml_reserved); |
64 |
64 |
65 fun warn_ml name = |
65 fun warn_ml name = |
66 if is_ml_identifier name then false |
66 if is_ml_identifier name then false |
|
67 else if name = "" then true |
67 else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
68 else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
68 |
69 |
69 fun ml_store_thm (name, thm) = |
70 fun ml_store_thm (name, thm) = |
70 let val thm' = store_thm (name, thm) in |
71 let val thm' = store_thm (name, thm) in |
71 if warn_ml name then () |
72 if warn_ml name then () |