--- a/src/Pure/Syntax/syntax.ML Wed Dec 13 15:47:36 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Dec 13 15:47:37 2006 +0100
@@ -40,7 +40,7 @@
type mode
val default_mode: mode
val input_mode: mode
- val internal_mode: mode
+ val internalM: string
val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
val extend_const_gram: (string -> bool) ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
@@ -188,7 +188,7 @@
type mode = string * bool;
val default_mode = ("", true);
val input_mode = ("input", true);
-val internal_mode = ("internal", true);
+val internalM = "internal";
(* empty_syntax *)