diff -r f6b6b2c55141 -r 9590df3c5f2a src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Oct 15 01:58:41 2003 +0200
+++ b/src/Pure/General/symbol.ML	Wed Oct 15 07:03:43 2003 +0200
@@ -110,7 +110,7 @@
 
     val bbb_letters = ["bool","complex","nat","rat","real","int"]
 
-    val control_letters = ["^sub"]
+    val control_letters = ["^isub", "^isup"]
  
     val pre_letters =
 	cal_letters   @