--- a/FSet.thy	Thu Nov 26 03:18:38 2009 +0100
+++ b/FSet.thy	Thu Nov 26 10:32:31 2009 +0100
@@ -342,7 +342,7 @@
 done
 
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+ML {* val app_prs_thms = map (applic_prs_old @{context} rty qty absrep) aps *}
 
 lemma cheat: "P" sorry
 
@@ -353,7 +353,7 @@
 ML {* Inductive.get_monos @{context} *}
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
+apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 defer
 apply(rule cheat)
 apply(rule cheat)
@@ -378,12 +378,12 @@
 done
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
+apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 defer
 apply(rule cheat)
 apply(rule cheat)
 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
-oops
+done
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"