--- a/quotient_def.ML	Fri Nov 06 11:02:11 2009 +0100
+++ b/quotient_def.ML	Fri Nov 06 19:26:08 2009 +0100
@@ -150,8 +150,8 @@
 
 fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
 let   
-  val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
-  val (_, rhs) = PrimitiveDefs.abs_def prop'
+  val (_, prop') = Primitive_Defs.dest_def lthy (K true) (K false) (K false) prop
+  val (_, rhs) = Primitive_Defs.abs_def prop'
 in
   make_def bind qty mx attr rhs lthy 
 end