diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/SubUnion.thy
--- a/src/ZF/Resid/SubUnion.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/SubUnion.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,10 +8,10 @@
 SubUnion = Redex +
 
 consts
-  Ssub,Scomp,Sreg  :: "i"
-  "<==","~"        :: "[i,i]=>o" (infixl 70)
-  un               :: "[i,i]=>i" (infixl 70)
-  regular	   :: "i=>o"
+  Ssub,Scomp,Sreg  :: i
+  "<==","~"        :: [i,i]=>o (infixl 70)
+  un               :: [i,i]=>i (infixl 70)
+  regular	   :: i=>o
   
 translations
   "a<==b"        == "<a,b>:Ssub"