Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Syntax/syntax_ext.ML
changeset 62529 8b7bdfc09f3b
parent 59841 2551ac44150e
child 62752 d09d71223e7a 
--- 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
isabelle