# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266249249 -3600
# Node ID a0e6d6b54509ea6d30b4a5984a241f4207983a2f
# Parent  7763756b42cffc4c42bcf32d00bca59baeaf59a3# Parent  368ec514aa34f37b3f5da460cf6def32576fdfb2
merge

diff -r 368ec514aa34 -r a0e6d6b54509 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Feb 15 16:52:32 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 15 16:54:09 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