--- a/QuotMain.thy	Thu Dec 03 13:45:52 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 13:56:59 2009 +0100
@@ -1091,7 +1091,7 @@
 fun clean_tac lthy quot =
   let
     val thy = ProofContext.theory_of lthy;
-    val defs = map (#def) (qconsts_dest thy);
+    val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
     val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot