diff -r 4cf79f70efec -r 3b3c5feb6b73 quotient.ML
--- a/quotient.ML	Thu Nov 12 12:07:33 2009 +0100
+++ b/quotient.ML	Thu Nov 12 13:56:07 2009 +0100
@@ -238,4 +238,4 @@
 
 end; (* structure *)
 
-open Quotient
\ No newline at end of file
+open Quotient