src/Pure/General/symbol_pos.ML
changeset 62529 8b7bdfc09f3b
parent 62239 6ee95b93fbed
child 62751 24e2b098bf44
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sun Mar 06 13:19:19 2016 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Mar 06 16:19:02 2016 +0100
     1.3 @@ -201,9 +201,9 @@
     1.4          ^ quote (content syms) ^ Position.here (#1 (range syms)));
     1.5    in
     1.6      (case syms of
     1.7 -      ("\\<open>", _) :: rest =>
     1.8 +      ("\<open>", _) :: rest =>
     1.9          (case rev rest of
    1.10 -          ("\\<close>", _) :: rrest => rev rrest
    1.11 +          ("\<close>", _) :: rrest => rev rrest
    1.12          | _ => err ())
    1.13      | _ => err ())
    1.14    end;
    1.15 @@ -279,7 +279,7 @@
    1.16  val letter = Scan.one (symbol #> Symbol.is_letter);
    1.17  val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
    1.18  
    1.19 -val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
    1.20 +val sub = Scan.one (symbol #> (fn s => s = "\<^sub>"));
    1.21  
    1.22  in
    1.23