| changeset 37146 | f652333bbf8e |
| parent 36739 | e9401d2efc5f |
| child 37216 | 3165bc303f66 |
--- a/src/Pure/Syntax/syntax.ML Thu May 27 17:41:27 2010 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu May 27 18:10:37 2010 +0200 @@ -259,7 +259,7 @@ type mode = string * bool; val mode_default = ("", true); -val mode_input = (PrintMode.input, true); +val mode_input = (Print_Mode.input, true); (* empty_syntax *)