--- a/Quot/QuotMain.thy	Fri Dec 11 19:22:30 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 01:44:56 2009 +0100
@@ -1,7 +1,7 @@
 theory QuotMain
 imports QuotScript Prove
 uses ("quotient_info.ML")
-     ("quotient.ML")
+     ("quotient_typ.ML")
      ("quotient_def.ML")
 begin
 
@@ -102,8 +102,7 @@
 lemmas [quot_equiv] = identity_equivp
 
 (* definition of the quotient types *)
-(* FIXME: should be called quotient_typ.ML *)
-use "quotient.ML"
+use "quotient_typ.ML"
 
 (* lifting of constants *)
 use "quotient_def.ML"