diff -r 5e92ce8f306d -r 3feed4dbfa45 quotient_def.ML
--- a/quotient_def.ML	Fri Dec 04 15:18:37 2009 +0100
+++ b/quotient_def.ML	Fri Dec 04 15:19:39 2009 +0100
@@ -118,7 +118,7 @@
 let   
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, rhs) = Primitive_Defs.abs_def prop'
-in
+in  
   make_def bind qty mx attr rhs lthy 
 end