diff -r 2ad8e66de294 -r 7763756b42cf Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Feb 15 16:51:30 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 15 16:53:51 2010 +0100
@@ -523,8 +523,7 @@
 *)
 fun clean_tac lthy =
 let
-  val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy)
-  (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+  val defs = map (symmetric o #def) (qconsts_dest lthy)
   val prs = prs_rules_get lthy
   val ids = id_simps_get lthy
   val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs