--- a/src/HOL/Quotient.thy Tue Nov 29 21:50:00 2011 +0100
+++ b/src/HOL/Quotient.thy Tue Nov 29 22:45:21 2011 +0100
@@ -8,7 +8,7 @@
imports Plain Hilbert_Choice Equiv_Relations
uses
("Tools/Quotient/quotient_info.ML")
- ("Tools/Quotient/quotient_typ.ML")
+ ("Tools/Quotient/quotient_type.ML")
("Tools/Quotient/quotient_def.ML")
("Tools/Quotient/quotient_term.ML")
("Tools/Quotient/quotient_tacs.ML")
@@ -696,7 +696,7 @@
text {* Definitions of the quotient types. *}
-use "Tools/Quotient/quotient_typ.ML"
+use "Tools/Quotient/quotient_type.ML"
text {* Definitions for quotient constants. *}