--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Dec 09 14:12:02 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Dec 09 14:14:37 2011 +0100
@@ -64,7 +64,7 @@
else error_msg binding lhs_str
| _ => raise Match)
- val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
+ val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'