changeset 4487 | 9b4c1db5aca1 |
parent 4147 | e57d03a5fc73 |
child 4699 | fc5687450acc |
--- a/src/Pure/Syntax/printer.ML Sun Dec 28 14:56:09 1997 +0100 +++ b/src/Pure/Syntax/printer.ML Sun Dec 28 14:56:44 1997 +0100 @@ -189,7 +189,7 @@ (*find tab for mode*) fun get_tab prtabs mode = - if_none (assoc (prtabs, mode)) Symtab.null; + if_none (assoc (prtabs, mode)) Symtab.empty; (*collect tabs for mode hierarchy (default "")*) fun tabs_of prtabs modes =