# HG changeset patch
# User wenzelm
# Date 1457277542 -3600
# Node ID 8b7bdfc09f3bd27fe32b889f9f5456dcb0791229
# Parent  c8c532b229477796c04835cf17e5eefdde7a0f1c
clarified treatment of fragments of Isabelle symbols during bootstrap;

diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/General/position.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -208,7 +208,7 @@
         (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
       | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
-      | _ => if is_reported pos then ("", "\\<here>") else ("", ""));
+      | _ => if is_reported pos then ("", "\<here>") else ("", ""));
   in
     if null props then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/General/symbol.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -95,8 +95,8 @@
 val STX = chr 2;
 val DEL = chr 127;
 
-val open_ = "\\<open>";
-val close = "\\<close>";
+val open_ = "\<open>";
+val close = "\<close>";
 
 val space = chr 32;
 
@@ -110,14 +110,14 @@
         Vector.sub (small_spaces, n mod 64);
 end;
 
-val comment = "\\<comment>";
+val comment = "\<comment>";
 
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
 fun raw_symbolic s =
-  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
+  String.isPrefix "\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\<^" s);
 
 fun is_symbolic s =
   s <> open_ andalso s <> close andalso raw_symbolic s;
@@ -129,7 +129,7 @@
   else is_utf8 s orelse raw_symbolic s;
 
 fun is_control s =
-  String.isPrefix "\\<^" s andalso String.isSuffix ">" s;
+  String.isPrefix "\<^" s andalso String.isSuffix ">" s;
 
 
 (* input source control *)
@@ -140,8 +140,8 @@
 val stopper = Scan.stopper (K eof) is_eof;
 
 fun is_malformed s =
-  String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
-  orelse s = "\\<>" orelse s = "\\<^>";
+  String.isPrefix "\<" s andalso not (String.isSuffix ">" s)
+  orelse s = "\<>" orelse s = "\<^>";
 
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
@@ -199,9 +199,9 @@
 fun encode_raw "" = ""
   | encode_raw str =
       let
-        val raw0 = enclose "\\<^raw:" ">";
+        val raw0 = enclose "\<^raw:" ">";
         val raw1 = raw0 o implode;
-        val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
+        val raw2 = enclose "\<^raw" ">" o string_of_int o ord;
 
         fun encode cs = enc (take_prefix raw_chr cs)
         and enc ([], []) = []
@@ -231,11 +231,11 @@
 (* decode_raw *)
 
 fun is_raw s =
-  String.isPrefix "\\<^raw" s andalso String.isSuffix ">" s;
+  String.isPrefix "\<^raw" s andalso String.isSuffix ">" s;
 
 fun decode_raw s =
   if not (is_raw s) then error (malformed_msg s)
-  else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
+  else if String.isPrefix "\<^raw:" s then String.substring (s, 7, size s - 8)
   else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
 
 
@@ -260,144 +260,144 @@
 local
   val letter_symbols =
     Symtab.make_set [
-      "\\<A>",
-      "\\<B>",
-      "\\<C>",
-      "\\<D>",
-      "\\<E>",
-      "\\<F>",
-      "\\<G>",
-      "\\<H>",
-      "\\<I>",
-      "\\<J>",
-      "\\<K>",
-      "\\<L>",
-      "\\<M>",
-      "\\<N>",
-      "\\<O>",
-      "\\<P>",
-      "\\<Q>",
-      "\\<R>",
-      "\\<S>",
-      "\\<T>",
-      "\\<U>",
-      "\\<V>",
-      "\\<W>",
-      "\\<X>",
-      "\\<Y>",
-      "\\<Z>",
-      "\\<a>",
-      "\\<b>",
-      "\\<c>",
-      "\\<d>",
-      "\\<e>",
-      "\\<f>",
-      "\\<g>",
-      "\\<h>",
-      "\\<i>",
-      "\\<j>",
-      "\\<k>",
-      "\\<l>",
-      "\\<m>",
-      "\\<n>",
-      "\\<o>",
-      "\\<p>",
-      "\\<q>",
-      "\\<r>",
-      "\\<s>",
-      "\\<t>",
-      "\\<u>",
-      "\\<v>",
-      "\\<w>",
-      "\\<x>",
-      "\\<y>",
-      "\\<z>",
-      "\\<AA>",
-      "\\<BB>",
-      "\\<CC>",
-      "\\<DD>",
-      "\\<EE>",
-      "\\<FF>",
-      "\\<GG>",
-      "\\<HH>",
-      "\\<II>",
-      "\\<JJ>",
-      "\\<KK>",
-      "\\<LL>",
-      "\\<MM>",
-      "\\<NN>",
-      "\\<OO>",
-      "\\<PP>",
-      "\\<QQ>",
-      "\\<RR>",
-      "\\<SS>",
-      "\\<TT>",
-      "\\<UU>",
-      "\\<VV>",
-      "\\<WW>",
-      "\\<XX>",
-      "\\<YY>",
-      "\\<ZZ>",
-      "\\<aa>",
-      "\\<bb>",
-      "\\<cc>",
-      "\\<dd>",
-      "\\<ee>",
-      "\\<ff>",
-      "\\<gg>",
-      "\\<hh>",
-      "\\<ii>",
-      "\\<jj>",
-      "\\<kk>",
-      "\\<ll>",
-      "\\<mm>",
-      "\\<nn>",
-      "\\<oo>",
-      "\\<pp>",
-      "\\<qq>",
-      "\\<rr>",
-      "\\<ss>",
-      "\\<tt>",
-      "\\<uu>",
-      "\\<vv>",
-      "\\<ww>",
-      "\\<xx>",
-      "\\<yy>",
-      "\\<zz>",
-      "\\<alpha>",
-      "\\<beta>",
-      "\\<gamma>",
-      "\\<delta>",
-      "\\<epsilon>",
-      "\\<zeta>",
-      "\\<eta>",
-      "\\<theta>",
-      "\\<iota>",
-      "\\<kappa>",
-      (*"\\<lambda>", sic!*)
-      "\\<mu>",
-      "\\<nu>",
-      "\\<xi>",
-      "\\<pi>",
-      "\\<rho>",
-      "\\<sigma>",
-      "\\<tau>",
-      "\\<upsilon>",
-      "\\<phi>",
-      "\\<chi>",
-      "\\<psi>",
-      "\\<omega>",
-      "\\<Gamma>",
-      "\\<Delta>",
-      "\\<Theta>",
-      "\\<Lambda>",
-      "\\<Xi>",
-      "\\<Pi>",
-      "\\<Sigma>",
-      "\\<Upsilon>",
-      "\\<Phi>",
-      "\\<Psi>",
-      "\\<Omega>"
+      "\<A>",
+      "\<B>",
+      "\<C>",
+      "\<D>",
+      "\<E>",
+      "\<F>",
+      "\<G>",
+      "\<H>",
+      "\<I>",
+      "\<J>",
+      "\<K>",
+      "\<L>",
+      "\<M>",
+      "\<N>",
+      "\<O>",
+      "\<P>",
+      "\<Q>",
+      "\<R>",
+      "\<S>",
+      "\<T>",
+      "\<U>",
+      "\<V>",
+      "\<W>",
+      "\<X>",
+      "\<Y>",
+      "\<Z>",
+      "\<a>",
+      "\<b>",
+      "\<c>",
+      "\<d>",
+      "\<e>",
+      "\<f>",
+      "\<g>",
+      "\<h>",
+      "\<i>",
+      "\<j>",
+      "\<k>",
+      "\<l>",
+      "\<m>",
+      "\<n>",
+      "\<o>",
+      "\<p>",
+      "\<q>",
+      "\<r>",
+      "\<s>",
+      "\<t>",
+      "\<u>",
+      "\<v>",
+      "\<w>",
+      "\<x>",
+      "\<y>",
+      "\<z>",
+      "\<AA>",
+      "\<BB>",
+      "\<CC>",
+      "\<DD>",
+      "\<EE>",
+      "\<FF>",
+      "\<GG>",
+      "\<HH>",
+      "\<II>",
+      "\<JJ>",
+      "\<KK>",
+      "\<LL>",
+      "\<MM>",
+      "\<NN>",
+      "\<OO>",
+      "\<PP>",
+      "\<QQ>",
+      "\<RR>",
+      "\<SS>",
+      "\<TT>",
+      "\<UU>",
+      "\<VV>",
+      "\<WW>",
+      "\<XX>",
+      "\<YY>",
+      "\<ZZ>",
+      "\<aa>",
+      "\<bb>",
+      "\<cc>",
+      "\<dd>",
+      "\<ee>",
+      "\<ff>",
+      "\<gg>",
+      "\<hh>",
+      "\<ii>",
+      "\<jj>",
+      "\<kk>",
+      "\<ll>",
+      "\<mm>",
+      "\<nn>",
+      "\<oo>",
+      "\<pp>",
+      "\<qq>",
+      "\<rr>",
+      "\<ss>",
+      "\<tt>",
+      "\<uu>",
+      "\<vv>",
+      "\<ww>",
+      "\<xx>",
+      "\<yy>",
+      "\<zz>",
+      "\<alpha>",
+      "\<beta>",
+      "\<gamma>",
+      "\<delta>",
+      "\<epsilon>",
+      "\<zeta>",
+      "\<eta>",
+      "\<theta>",
+      "\<iota>",
+      "\<kappa>",
+      (*"\<lambda>", sic!*)
+      "\<mu>",
+      "\<nu>",
+      "\<xi>",
+      "\<pi>",
+      "\<rho>",
+      "\<sigma>",
+      "\<tau>",
+      "\<upsilon>",
+      "\<phi>",
+      "\<chi>",
+      "\<psi>",
+      "\<omega>",
+      "\<Gamma>",
+      "\<Delta>",
+      "\<Theta>",
+      "\<Lambda>",
+      "\<Xi>",
+      "\<Pi>",
+      "\<Sigma>",
+      "\<Upsilon>",
+      "\<Phi>",
+      "\<Psi>",
+      "\<Omega>"
     ];
 in
 
@@ -421,7 +421,7 @@
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
-val is_block_ctrl = member (op =) ["\\<^bsub>", "\\<^esub>", "\\<^bsup>", "\\<^esup>"];
+val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
 
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
@@ -531,7 +531,7 @@
 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
-fun symbolic_end (_ :: "\\<^sub>" :: _) = true
+fun symbolic_end (_ :: "\<^sub>" :: _) = true
   | symbolic_end ("'" :: ss) = symbolic_end ss
   | symbolic_end (s :: _) = raw_symbolic s
   | symbolic_end [] = false;
@@ -561,8 +561,8 @@
 
 fun sym_len s =
   if not (is_printable s) then (0: int)
-  else if String.isPrefix "\\<long" s then 2
-  else if String.isPrefix "\\<Long" s then 2
+  else if String.isPrefix "\<long" s then 2
+  else if String.isPrefix "\<Long" s then 2
   else 1;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -201,9 +201,9 @@
         ^ quote (content syms) ^ Position.here (#1 (range syms)));
   in
     (case syms of
-      ("\\<open>", _) :: rest =>
+      ("\<open>", _) :: rest =>
         (case rev rest of
-          ("\\<close>", _) :: rrest => rev rrest
+          ("\<close>", _) :: rrest => rev rrest
         | _ => err ())
     | _ => err ())
   end;
@@ -279,7 +279,7 @@
 val letter = Scan.one (symbol #> Symbol.is_letter);
 val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
 
-val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
+val sub = Scan.one (symbol #> (fn s => s = "\<^sub>"));
 
 in
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Isar/parse.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -211,7 +211,7 @@
   group (fn () => "reserved identifier " ^ quote x)
     (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
-val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
+val dots = sym_ident :-- (fn "\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
 
 val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -31,13 +31,14 @@
   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   else s;
 
-fun ml_positions start_line name txt =
+fun ml_input start_line name txt =
   let
     fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
           let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
           in positions line cs (s :: res) end
-      | positions line (c :: cs) res =
-          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+      | positions line (#"\\" :: #"<" :: cs) res = positions line cs ("\\\\<" :: res)
+      | positions line (#"\n" :: cs) res = positions (line + 1) cs ("\n" :: res)
+      | positions line (c :: cs) res = positions line cs (str c :: res)
       | positions _ [] res = rev res;
   in String.concat (positions start_line (String.explode txt) []) end;
 
@@ -46,7 +47,7 @@
     val _ = Secure.deny_ml ();
 
     val current_line = Unsynchronized.ref line;
-    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
+    val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
     val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -304,7 +304,7 @@
 
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     fun chop_idx [] ds = idxname [] ds
-      | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
+      | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds
       | chop_idx (c :: cs) ds =
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;
@@ -426,10 +426,10 @@
 
 fun marker s = (prefix s, unprefix s);
 
-val (mark_class, unmark_class) = marker "\\<^class>";
-val (mark_type, unmark_type) = marker "\\<^type>";
-val (mark_const, unmark_const) = marker "\\<^const>";
-val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
+val (mark_class, unmark_class) = marker "\<^class>";
+val (mark_type, unmark_type) = marker "\<^type>";
+val (mark_const, unmark_const) = marker "\<^const>";
+val (mark_fixed, unmark_fixed) = marker "\<^fixed>";
 
 fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
   (case try unmark_class s of
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -140,7 +140,7 @@
 
 local
 
-val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
+val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
 
 val scan_delim_char =
   $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
@@ -151,7 +151,7 @@
 
 val scan_sym =
   $$ "_" >> K (Argument ("", 0)) ||
-  $$ "\\<index>" >> K index ||
+  $$ "\<index>" >> K index ||
   $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
   $$ ")" >> K En ||
   $$ "/" -- $$ "/" >> K (Brk ~1) ||
@@ -168,7 +168,7 @@
 
 fun unique_index xsymbs =
   if length (filter is_index xsymbs) <= 1 then xsymbs
-  else error "Duplicate index arguments (\\<index>)";
+  else error "Duplicate index arguments (\<index>)";
 
 in
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -179,7 +179,7 @@
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
-      | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
+      | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
       | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
@@ -797,7 +797,7 @@
 
 (* type propositions *)
 
-fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
+fun type_prop_tr' ctxt T [Const ("\<^const>Pure.sort_constraint", _)] =
       Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   | type_prop_tr' ctxt T [t] =
       Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
@@ -839,7 +839,7 @@
     ("_context_xconst", const_ast_tr false)] #>
   Sign.typed_print_translation
    [("_type_prop", type_prop_tr'),
-    ("\\<^const>Pure.type", type_tr'),
+    ("\<^const>Pure.type", type_tr'),
     ("_type_constraint_", type_constraint_tr')]);
 
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -102,7 +102,7 @@
 fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
   | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
 
-fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
+fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
 
 
@@ -152,18 +152,18 @@
 
 fun mk_type ty =
   Syntax.const "_constrain" $
-    Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty);
+    Syntax.const "\<^const>Pure.type" $ (Syntax.const "\<^type>itself" $ ty);
 
 fun ofclass_tr [ty, cls] = cls $ mk_type ty
   | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
 
-fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
+fun sort_constraint_tr [ty] = Syntax.const "\<^const>Pure.sort_constraint" $ mk_type ty
   | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
 
 
 (* meta propositions *)
 
-fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
+fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\<^type>prop"
   | aprop_tr ts = raise TERM ("aprop_tr", ts);
 
 
@@ -174,7 +174,7 @@
         (case Ast.unfold_ast_p "_asms" asms of
           (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
         | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
-      in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
+      in Ast.fold_ast_p "\<^const>Pure.imp" (prems, concl) end
   | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
 
 
@@ -273,7 +273,7 @@
 fun fun_ast_tr' asts =
   if no_brackets () orelse no_type_brackets () then raise Match
   else
-    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
+    (case Ast.unfold_ast_p "\<^type>fun" (Ast.Appl (Ast.Constant "\<^type>fun" :: asts)) of
       (dom as _ :: _ :: _, cod)
         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
     | _ => raise Match);
@@ -389,8 +389,8 @@
 fun impl_ast_tr' asts =
   if no_brackets () then raise Match
   else
-    (case Ast.unfold_ast_p "\\<^const>Pure.imp"
-        (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
+    (case Ast.unfold_ast_p "\<^const>Pure.imp"
+        (Ast.Appl (Ast.Constant "\<^const>Pure.imp" :: asts)) of
       (prems as _ :: _ :: _, concl) =>
         let
           val (asms, asm) = split_last prems;
@@ -501,11 +501,11 @@
   ("_struct", struct_tr)];
 
 val pure_print_ast_translation =
- [("\\<^type>fun", fn _ => fun_ast_tr'),
+ [("\<^type>fun", fn _ => fun_ast_tr'),
   ("_abs", fn _ => abs_ast_tr'),
   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
-  ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
+  ("\<^const>Pure.imp", fn _ => impl_ast_tr'),
   ("_index", fn _ => index_ast_tr'),
   ("_struct", struct_ast_tr')];
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Thy/html.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -39,10 +39,10 @@
     val mapping =
       map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @
        [("'", "&#39;"),
-        ("\\<^bsub>", hidden "&#8664;" ^ "<sub>"),
-        ("\\<^esub>", hidden "&#8665;" ^ "</sub>"),
-        ("\\<^bsup>", hidden "&#8663;" ^ "<sup>"),
-        ("\\<^esup>", hidden "&#8662;" ^ "</sup>")];
+        ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
+        ("\<^esub>", hidden "&#8665;" ^ "</sub>"),
+        ("\<^bsup>", hidden "&#8663;" ^ "<sup>"),
+        ("\<^esup>", hidden "&#8662;" ^ "</sup>")];
   in Symbols (fold Symtab.update mapping Symtab.empty) end;
 
 val no_symbols = make_symbols [];
@@ -70,9 +70,9 @@
       let
         val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
         val (s, r) =
-          if s1 = "\\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
-          else if s1 = "\\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
-          else if s1 = "\\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
+          if s1 = "\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
+          else if s1 = "\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
+          else if s1 = "\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
           else (output_sym symbols s1, rest);
       in output_syms symbols r (s :: result) end;
 
@@ -120,19 +120,19 @@
 (* document *)
 
 fun begin_document symbols title =
-  "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
-  \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
-  \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
-  \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
-  \<head>\n\
-  \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
-  \<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
-  \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
-  \</head>\n\
-  \\n\
-  \<body>\n\
-  \<div class=\"head\">\
-  \<h1>" ^ output symbols title ^ "</h1>\n";
+  "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" ^
+  "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
+  "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
+  "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
+  "<head>\n" ^
+  "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
+  "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
+  "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
+  "</head>\n" ^
+  "\n" ^
+  "<body>\n" ^
+  "<div class=\"head\">" ^
+  "<h1>" ^ output symbols title ^ "</h1>\n";
 
 val end_document = "\n</div>\n</body>\n</html>\n";
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/Thy/markdown.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -49,7 +49,7 @@
 
 val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
 
-val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
+val is_control = member (op =) ["\<^item>", "\<^enum>", "\<^descr>"];
 
 
 (* document lines *)
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/library.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -693,7 +693,7 @@
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";
 
-val cartouche = enclose "\\<open>" "\\<close>";
+val cartouche = enclose "\<open>" "\<close>";
 
 val space_implode = String.concatWith;
 
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/pure_thy.ML	Sun Mar 06 16:19:02 2016 +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 ("(_/ \\<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 "_,/ _"),
@@ -131,26 +131,26 @@
     ("",            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),
@@ -189,9 +189,9 @@
   #> 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 "'_")]
diff -r c8c532b22947 -r 8b7bdfc09f3b src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/term.ML	Sun Mar 06 16:19:02 2016 +0100
@@ -986,7 +986,7 @@
     val idx = string_of_int i;
     val dot =
       (case rev (Symbol.explode x) of
-        _ :: "\\<^sub>" :: _ => false
+        _ :: "\<^sub>" :: _ => false
       | c :: _ => Symbol.is_digit c
       | _ => true);
   in