diff -r 38b73f7940af -r 301833d9013a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Dec 28 23:13:33 2015 +0100
+++ b/src/Pure/pure_thy.ML	Tue Dec 29 14:58:15 2015 +0100
@@ -108,12 +108,12 @@
     ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
     ("",            typ "type => types",               Delimfix "_"),
     ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
-    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ => _)", [1, 0], 0)),
-    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ => _)", [0, 0], 0)),
+    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
     ("",            typ "type => type",                Delimfix "'(_')"),
     ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
     ("_type_prop",  typ "'a",                          NoSyn),
-    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
+    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     ("_abs",        typ "'a",                          NoSyn),
     ("",            typ "'a => args",                  Delimfix "_"),
     ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
@@ -131,18 +131,18 @@
     ("",            typ "id_position => aprop",        Delimfix "_"),
     ("",            typ "longid_position => aprop",    Delimfix "_"),
     ("",            typ "var_position => aprop",       Delimfix "_"),
-    ("_DDDOT",      typ "aprop",                       Delimfix "..."),
+    ("_DDDOT",      typ "aprop",                       Delimfix "\\<dots>"),
     ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
     ("_asm",        typ "prop => asms",                Delimfix "_"),
     ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
-    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
     ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
     ("_mk_ofclass", typ "dummy",                       NoSyn),
     ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
     ("",            typ "id_position => logic",        Delimfix "_"),
     ("",            typ "longid_position => logic",    Delimfix "_"),
     ("",            typ "var_position => logic",       Delimfix "_"),
-    ("_DDDOT",      typ "logic",                       Delimfix "..."),
+    ("_DDDOT",      typ "logic",                       Delimfix "\\<dots>"),
     ("_strip_positions", typ "'a", NoSyn),
     ("_position",   typ "num_token => num_position",   Delimfix "_"),
     ("_position",   typ "float_token => float_position", Delimfix "_"),
@@ -171,30 +171,27 @@
     ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
     ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
     ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
-    (const "Pure.imp",  typ "prop => prop => prop",     Delimfix "op ==>"),
     (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
     ("_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 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)),
-    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
-    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
-    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
-    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
-    ("_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_syntax (Print_Mode.ASCII, true)
+   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ => _)", [1, 0], 0)),
+    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ => _)", [0, 0], 0)),
+    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3%_./ _)", [0, 3], 3)),
+    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("==", 2)),
+    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)),
+    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("==>", 1)),
+    ("_DDDOT",            typ "aprop",                  Delimfix "..."),
+    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+    ("_DDDOT",            typ "logic",                  Delimfix "...")]
   #> Sign.add_syntax ("", false)
    [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
-  #> Sign.add_syntax ("HTML", false)
-   [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   #> Sign.add_consts
-   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("==", 2)),
-    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
-    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
+   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
+    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\<And>", 0, 0)),
     (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
     (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
     (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]