| changeset 16894 | 40f80823b451 |
| parent 16345 | b035482bed02 |
| child 17030 | ab8c7fbf235b |
--- a/src/Pure/Isar/isar_output.ML Tue Jul 19 20:47:00 2005 +0200 +++ b/src/Pure/Isar/isar_output.ML Tue Jul 19 20:47:01 2005 +0200 @@ -60,7 +60,7 @@ fun add_item kind (tab, (name, x)) = - (if is_none (Symtab.lookup (tab, name)) then () + (if not (Symtab.defined tab name) then () else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name); Symtab.update ((name, x), tab));