--- a/FSet.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/FSet.thy	Sat Nov 28 05:47:13 2009 +0100
@@ -445,6 +445,7 @@
   done
 
 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun r_mk_comb_tac_fset' lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 (* 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"
@@ -462,6 +463,8 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)

--- a/QuotMain.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:47:13 2009 +0100
@@ -729,6 +729,24 @@
      | _ => no_tac)
 *}
 
+ML {*
+val ball_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+            rtac @{thm FUN_REL_I} 1
+      |_ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+            rtac @{thm FUN_REL_I} 1
+      | _ => no_tac)
+*}
+
 ML {* (* Legacy *)
 fun needs_lift (rty as Type (rty_s, _)) ty =
   case ty of
@@ -755,30 +773,6 @@
 *}
 
 ML {*
-val ball_rsp_tac = 
-  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-     case (term_of concl) of
-        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
-            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-            THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-      |_ => no_tac)
-*}
-
-ML {*
-val bex_rsp_tac = 
-  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-     case (term_of concl) of
-        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
-            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-            THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-      | _ => no_tac)
-*}
-
-ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            LAMBDA_RES_TAC ctxt,
@@ -839,11 +833,16 @@
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
     DT ctxt "2" (LAMBDA_RES_TAC ctxt),
 
-    (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
+    (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
 
+    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
     DT ctxt "4" (ball_rsp_tac ctxt),
+
+    (* = (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
     DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+
+    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
     DT ctxt "6" (bex_rsp_tac ctxt),
 
     (* respectfulness of ops *)