--- a/QuotMain.thy	Sat Nov 28 06:14:50 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 06:15:06 2009 +0100
@@ -827,6 +827,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
@@ -853,30 +871,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 SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 *}
 
@@ -941,11 +935,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 *)