--- a/FSet.thy	Mon Nov 30 12:26:08 2009 +0100
+++ b/FSet.thy	Mon Nov 30 13:58:05 2009 +0100
@@ -295,8 +295,7 @@
 
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val rsp_thms =
-  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
-  @ @{thms ho_all_prs ho_ex_prs} *}
+  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
@@ -506,20 +505,20 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply assumption
 apply (rule refl)
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})