# 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 *)