--- a/src/Pure/General/symbol.ML Mon Oct 13 16:54:20 2003 +0200
+++ b/src/Pure/General/symbol.ML Wed Oct 15 01:52:47 2003 +0200
@@ -110,13 +110,17 @@
val bbb_letters = ["bool","complex","nat","rat","real","int"]
+ val control_letters = ["^sub"]
+
val pre_letters =
cal_letters @
small_letters @
goth_letters @
- greek_letters
+ greek_letters @
+ control_letters
+
in
-val ext_letters = map wrap pre_letters
+val ext_letters = map wrap pre_letters
fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
end