# HG changeset patch
# User wenzelm
# Date 850218542 -3600
# Node ID 97b88cafe1e81989912edd6c63690d943de0c0e2
# Parent  2106d61252b6e149b457996a6cdd25ddee4cecab
add_modesyntax(_i): added 'inout' argument;

diff -r 2106d61252b6 -r 97b88cafe1e8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Dec 10 12:17:11 1996 +0100
+++ b/src/Pure/sign.ML	Tue Dec 10 12:49:02 1996 +0100
@@ -51,8 +51,8 @@
   val add_consts_i: (string * typ * mixfix) list -> sg -> sg
   val add_syntax: (string * string * mixfix) list -> sg -> sg
   val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
-  val add_modesyntax: string * (string * string * mixfix) list -> sg -> sg
-  val add_modesyntax_i: string * (string * typ * mixfix) list -> sg -> sg
+  val add_modesyntax: (string * bool) * (string * string * mixfix) list -> sg -> sg
+  val add_modesyntax_i: (string * bool) * (string * typ * mixfix) list -> sg -> sg
   val add_trfuns:
     (string * (ast list -> ast)) list *
     (string * (term list -> term)) list *
@@ -469,10 +469,10 @@
         handle Symtab.DUPS cs => err_dup_consts cs)
   end;
 
-val ext_consts_i = ext_cnsts (K (K I)) false "";
-val ext_consts = ext_cnsts read_const false "";
-val ext_syntax_i = ext_cnsts (K (K I)) true "";
-val ext_syntax = ext_cnsts read_const true "";
+val ext_consts_i = ext_cnsts (K (K I)) false ("", true);
+val ext_consts = ext_cnsts read_const false ("", true);
+val ext_syntax_i = ext_cnsts (K (K I)) true ("", true);
+val ext_syntax = ext_cnsts read_const true ("", true);
 fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts (K (K I)) true prmode sg consts;
 fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts;
 
@@ -611,7 +611,7 @@
     ("prop", [], logicS),
     ("itself", [logicS], logicS)]
   |> add_syntax Syntax.pure_syntax
-  |> add_modesyntax ("symbols", Syntax.pure_sym_syntax)
+  |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
   |> add_trfuns Syntax.pure_trfuns
   |> add_consts
    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
diff -r 2106d61252b6 -r 97b88cafe1e8 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Dec 10 12:17:11 1996 +0100
+++ b/src/Pure/theory.ML	Tue Dec 10 12:49:02 1996 +0100
@@ -36,8 +36,8 @@
   val add_consts_i	: (string * typ * mixfix) list -> theory -> theory
   val add_syntax	: (string * string * mixfix) list -> theory -> theory
   val add_syntax_i	: (string * typ * mixfix) list -> theory -> theory
-  val add_modesyntax	: string -> (string * string * mixfix) list -> theory -> theory
-  val add_modesyntax_i	: string -> (string * typ * mixfix) list -> theory -> theory
+  val add_modesyntax	: string * bool -> (string * string * mixfix) list -> theory -> theory
+  val add_modesyntax_i	: string * bool -> (string * typ * mixfix) list -> theory -> theory
   val add_trfuns	:
     (string * (Syntax.ast list -> Syntax.ast)) list *
     (string * (term list -> term)) list *