1.1 --- a/src/Pure/sign.ML	Tue Dec 10 12:17:11 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 10 12:49:02 1996 +0100
     1.3 @@ -51,8 +51,8 @@
     1.4    val add_consts_i: (string * typ * mixfix) list -> sg -> sg
     1.5    val add_syntax: (string * string * mixfix) list -> sg -> sg
     1.6    val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
     1.7 -  val add_modesyntax: string * (string * string * mixfix) list -> sg -> sg
     1.8 -  val add_modesyntax_i: string * (string * typ * mixfix) list -> sg -> sg
     1.9 +  val add_modesyntax: (string * bool) * (string * string * mixfix) list -> sg -> sg
    1.10 +  val add_modesyntax_i: (string * bool) * (string * typ * mixfix) list -> sg -> sg
    1.11    val add_trfuns:
    1.12      (string * (ast list -> ast)) list *
    1.13      (string * (term list -> term)) list *
    1.14 @@ -469,10 +469,10 @@
    1.15          handle Symtab.DUPS cs => err_dup_consts cs)
    1.16    end;
    1.17  
    1.18 -val ext_consts_i = ext_cnsts (K (K I)) false "";
    1.19 -val ext_consts = ext_cnsts read_const false "";
    1.20 -val ext_syntax_i = ext_cnsts (K (K I)) true "";
    1.21 -val ext_syntax = ext_cnsts read_const true "";
    1.22 +val ext_consts_i = ext_cnsts (K (K I)) false ("", true);
    1.23 +val ext_consts = ext_cnsts read_const false ("", true);
    1.24 +val ext_syntax_i = ext_cnsts (K (K I)) true ("", true);
    1.25 +val ext_syntax = ext_cnsts read_const true ("", true);
    1.26  fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts (K (K I)) true prmode sg consts;
    1.27  fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts;
    1.28  
    1.29 @@ -611,7 +611,7 @@
    1.30      ("prop", [], logicS),
    1.31      ("itself", [logicS], logicS)]
    1.32    |> add_syntax Syntax.pure_syntax
    1.33 -  |> add_modesyntax ("symbols", Syntax.pure_sym_syntax)
    1.34 +  |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
    1.35    |> add_trfuns Syntax.pure_trfuns
    1.36    |> add_consts
    1.37     [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),

     2.1 --- a/src/Pure/theory.ML	Tue Dec 10 12:17:11 1996 +0100
     2.2 +++ b/src/Pure/theory.ML	Tue Dec 10 12:49:02 1996 +0100
     2.3 @@ -36,8 +36,8 @@
     2.4    val add_consts_i	: (string * typ * mixfix) list -> theory -> theory
     2.5    val add_syntax	: (string * string * mixfix) list -> theory -> theory
     2.6    val add_syntax_i	: (string * typ * mixfix) list -> theory -> theory
     2.7 -  val add_modesyntax	: string -> (string * string * mixfix) list -> theory -> theory
     2.8 -  val add_modesyntax_i	: string -> (string * typ * mixfix) list -> theory -> theory
     2.9 +  val add_modesyntax	: string * bool -> (string * string * mixfix) list -> theory -> theory
    2.10 +  val add_modesyntax_i	: string * bool -> (string * typ * mixfix) list -> theory -> theory
    2.11    val add_trfuns	:
    2.12      (string * (Syntax.ast list -> Syntax.ast)) list *
    2.13      (string * (term list -> term)) list *