diff -r 6642df770bc4 -r 30fb2ca89773 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Feb 16 15:12:31 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Feb 16 15:13:14 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