# HG changeset patch
# User wenzelm
# Date 1192899275 -7200
# Node ID f37d7dd25c8856306cb6471398acd2ae58378b04
# Parent  fbea3ca04d51ceec2662f33a2eaa0c7f2dbe3940
moved internalM to PrintMode.internal;
PrintMode.input;

diff -r fbea3ca04d51 -r f37d7dd25c88 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Oct 20 18:54:34 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Oct 20 18:54:35 2007 +0200
@@ -41,7 +41,6 @@
   type mode
   val mode_default: mode
   val mode_input: 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
@@ -254,8 +253,7 @@
 
 type mode = string * bool;
 val mode_default = ("", true);
-val mode_input = ("input", true);
-val internalM = "internal";
+val mode_input = (PrintMode.input, true);
 
 
 (* empty_syntax *)