src/Pure/General/symbol_pos.ML
changeset 62529 8b7bdfc09f3b
parent 62239 6ee95b93fbed
child 62751 24e2b098bf44
--- 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