diff -r 42b90994ac77 -r 89d772dae4d4 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Jan 08 15:02:12 2010 +0100
+++ b/Quot/quotient_def.ML	Fri Jan 08 19:46:22 2010 +0100
@@ -40,7 +40,7 @@
 let
   val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
   val qconst_bname = Binding.name lhs_str;
-  val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
+  val absrep_trm = Syntax.check_term lthy (absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs)
   val prop = Logic.mk_equals (lhs, absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'