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/lexicon.ML
changeset 62529 8b7bdfc09f3b
parent 61476 1884c40f1539
child 62663 bea354f6ff21 
--- 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
isabelle