# HG changeset patch
# User wenzelm
# Date 1165683952 -3600
# Node ID 360fa2caaf2f9f72d1d630119511980d0b4ae89d
# Parent  88d8b40527920f28cd070b7f10411a81a1a35ff8
added internal_mode;

diff -r 88d8b4052792 -r 360fa2caaf2f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Dec 09 18:05:50 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 09 18:05:52 2006 +0100
@@ -40,6 +40,7 @@
   type mode
   val default_mode: mode
   val input_mode: mode
+  val internal_mode: mode
   val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
   val extend_const_gram: (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
@@ -187,6 +188,7 @@
 type mode = string * bool;
 val default_mode = ("", true);
 val input_mode = ("input", true);
+val internal_mode = ("internal", true);
 
 
 (* empty_syntax *)