--- a/Quot/Examples/FSet.thy	Tue Dec 08 17:34:10 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:40:58 2009 +0100
@@ -430,15 +430,12 @@
 sorry
 
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
-apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
+apply(lifting ttt2)
+apply(regularize)
 apply(rule impI)
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"

--- a/Quot/QuotMain.thy	Tue Dec 08 17:34:10 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:40:58 2009 +0100
@@ -1055,7 +1055,7 @@
     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 = @{thms all_prs ex_prs} @ defs
+    val thms1 = @{thms all_prs ex_prs} @ defs @ (prs_rules_get lthy) 
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
                 @ @{thms Quotient_abs_rep Quotient_rel_rep} 
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver