src/Pure/General/symbol.ML
changeset 14232 ef550525c591
parent 14221 9276f30eaed6
child 14234 9590df3c5f2a
--- 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