--- a/Quot/Examples/LFex.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/LFex.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -73,11 +73,12 @@
   and   "equivp atrm"
 sorry
 
-quotient KIND = kind / akind
+quotient_type KIND = kind / akind
   by (rule alpha_equivps)
 
-quotient TY = ty / aty
-   and   TRM = trm / atrm
+quotient_type 
+    TY = ty / aty and   
+    TRM = trm / atrm
   by (auto intro: alpha_equivps)
 
 quotient_def