--- a/src/Pure/pure_thy.ML Fri Mar 21 10:45:03 2014 +0100
+++ b/src/Pure/pure_thy.ML Fri Mar 21 11:06:39 2014 +0100
@@ -49,8 +49,8 @@
val old_appl_syntax_setup =
Old_Appl_Syntax.put true #>
- Sign.del_modesyntax Syntax.mode_default applC_syntax #>
- Sign.add_syntax appl_syntax;
+ Sign.del_syntax Syntax.mode_default applC_syntax #>
+ Sign.add_syntax Syntax.mode_default appl_syntax;
(* main content *)
@@ -75,8 +75,8 @@
"tvar_position", "id_position", "longid_position", "var_position",
"str_position", "string_position", "cartouche_position", "type_name",
"class_name"]))
- #> Sign.add_syntax (map (fn x => (x, typ "'a", NoSyn)) token_markers)
- #> Sign.add_syntax
+ #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
+ #> Sign.add_syntax Syntax.mode_default
[("", typ "prop' => prop", Delimfix "_"),
("", typ "logic => any", Delimfix "_"),
("", typ "prop' => any", Delimfix "_"),
@@ -174,8 +174,8 @@
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
- #> Sign.add_syntax applC_syntax
- #> Sign.add_modesyntax (Symbol.xsymbolsN, true)
+ #> Sign.add_syntax Syntax.mode_default applC_syntax
+ #> Sign.add_syntax (Symbol.xsymbolsN, true)
[(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
@@ -190,9 +190,9 @@
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
- #> Sign.add_modesyntax ("", false)
+ #> Sign.add_syntax ("", false)
[(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
- #> Sign.add_modesyntax ("HTML", false)
+ #> Sign.add_syntax ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts
[(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),