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 *