diff -r 0b60d8416ec5 -r 8237786171f1 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/quotient_tacs.ML	Fri Dec 25 00:58:06 2009 +0100
@@ -504,18 +504,21 @@
 
 fun clean_tac_aux lthy =
 let
+  (*FIXME produce defs with lthy, like prs and ids *)
   val thy = ProofContext.theory_of lthy;
   val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
-      (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
-    
-  val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
-  val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) 
-  fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+   (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+  val prs = prs_rules_get lthy
+  val ids = id_simps_get lthy
+  
+  fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+  val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
+  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) 
 in
-  EVERY' [simp_tac (simps thms1),
+  EVERY' [simp_tac ss1,
           fun_map_tac lthy,
           lambda_prs_tac lthy,
-          simp_tac (simps thms2),
+          simp_tac ss2,
           TRY o rtac refl]  
 end