diff -r fafcc54e531d -r 7ef153ded7e2 FSet.thy
--- a/FSet.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/FSet.thy	Thu Nov 26 20:32:33 2009 +0100
@@ -341,9 +341,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val app_prs_thms = map (applic_prs_old @{context} rty qty absrep) aps *}
-
 lemma cheat: "P" sorry
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
@@ -352,6 +349,7 @@
 prefer 2
 apply(rule cheat)
 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
+sorry
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
@@ -407,7 +405,7 @@
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+apply (tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)