--- a/Quot/quotient_def.ML	Tue Feb 09 14:32:37 2010 +0100
+++ b/Quot/quotient_def.ML	Tue Feb 09 15:28:15 2010 +0100
@@ -53,7 +53,7 @@
   val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
 
   val qconst_bname = Binding.name lhs_str
-  val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
+  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 (_, newrhs) = Primitive_Defs.abs_def prop'