# HG changeset patch # User wenzelm # Date 1166021257 -3600 # Node ID b90d927e0a4b3d9365bea6934f2e500b03551045 # Parent 6f6bf23f4c1e6331763c182b1ed16164cf70579b tuned signature; diff -r 6f6bf23f4c1e -r b90d927e0a4b src/Pure/Syntax/syntax.ML --- 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 *)