diff -r d0250d01782c -r df053507edba Quot/Examples/LFex.thy
--- 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