1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Oct 20 18:54:34 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Oct 20 18:54:35 2007 +0200
     1.3 @@ -41,7 +41,6 @@
     1.4    type mode
     1.5    val mode_default: mode
     1.6    val mode_input: mode
     1.7 -  val internalM: string
     1.8    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
     1.9    val extend_const_gram: (string -> bool) ->
    1.10      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.11 @@ -254,8 +253,7 @@
    1.12  
    1.13  type mode = string * bool;
    1.14  val mode_default = ("", true);
    1.15 -val mode_input = ("input", true);
    1.16 -val internalM = "internal";
    1.17 +val mode_input = (PrintMode.input, true);
    1.18  
    1.19  
    1.20  (* empty_syntax *)