diff -r 3413aa899aa7 -r c1e76f09db70 FSet.thy
--- a/FSet.thy	Sat Oct 24 08:09:40 2009 +0200
+++ b/FSet.thy	Sat Oct 24 08:24:26 2009 +0200
@@ -326,7 +326,7 @@
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
     (
-     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps res_thms))
+     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs})))
      THEN_ALL_NEW (fn _ => no_tac)
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
@@ -358,13 +358,11 @@
 ML_prf {* val ctxt = @{context} *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
-prefer 2
 apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
 prove list_induct_t: trm
@@ -389,7 +387,6 @@
 prove m2_t_p: m2_t_g
 apply (atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
 prove m2_t: m2_t