--- a/Attic/Quot/quotient_def.ML	Thu Mar 04 15:56:58 2010 +0100
+++ b/Attic/Quot/quotient_def.ML	Sun Mar 07 21:30:12 2010 +0100
@@ -63,7 +63,7 @@
   val qconst_bname = Binding.name lhs_str
   val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
-  val (_, prop') = LocalDefs.cert_def lthy prop
+  val (_, prop') = Local_Defs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'
 
   val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy