src/Pure/pure_thy.ML

     ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
     ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [1000, 0], 1000)),
     ("_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 ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
-    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \\<Rightarrow> _)", [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>dummy", typ "type",                      Delimfix "'_"),
     ("_type_prop",  typ "'a",                          NoSyn),
-    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\\<lambda>_./ _)", [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 "_,/ _"),
     ("",            typ "id_position => idt",          Delimfix "_"),
     ("_idtdummy",   typ "idt",                         Delimfix "'_"),

     ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
     ("",            typ "aprop => aprop",              Delimfix "'(_')"),
     ("",            typ "id_position => aprop",        Delimfix "_"),
     ("",            typ "longid_position => aprop",    Delimfix "_"),
     ("",            typ "var_position => aprop",       Delimfix "_"),
-    ("_DDDOT",      typ "aprop",                       Delimfix "\\<dots>"),
+    ("_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 ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [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 "\\<dots>"),
+    ("_DDDOT",      typ "logic",                       Delimfix "\<dots>"),
     ("_strip_positions", typ "'a", NoSyn),
     ("_position",   typ "num_token => num_position",   Delimfix "_"),
     ("_position",   typ "float_token => float_position", Delimfix "_"),
     ("_constify",   typ "num_position => num_const",   Delimfix "_"),
     ("_constify",   typ "float_position => float_const", Delimfix "_"),
-    ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
+    ("_index",      typ "logic => index",              Delimfix "(00\<^bsub>_\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
-    ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
+    ("_indexvar",   typ "index",                       Delimfix "'\<index>"),
     ("_struct",     typ "index => logic",              NoSyn),
     ("_update_name", typ "idt",                        NoSyn),
     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position_sort", typ "tid => tid_position",      Delimfix "_"),
     ("_position_sort", typ "tvar => tvar_position",    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_consts
-   [(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 ("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 "'_")]
   #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
   #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []