diff -r d1aa26ecfecd -r 021d9e4e5cc1 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 05:49:16 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:53:31 2009 +0100
@@ -871,62 +871,10 @@
 *}
 
 ML {*
-<<<<<<< variant A
->>>>>>> variant B
-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)
 *}
 
 ML {*
-####### Ancestor
-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 {*
-======= end
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            LAMBDA_RES_TAC ctxt,