--- a/QuotMain.thy	Mon Dec 07 01:22:20 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 01:28:10 2009 +0100
@@ -521,54 +521,6 @@
 *}
 
 ML {*
-fun ball_reg_eqv_simproc ss redex =
-  let
-    val ctxt = Simplifier.the_context ss
-    val thy = ProofContext.theory_of ctxt
-  in
-  case redex of
-      (ogl as ((Const (@{const_name "Ball"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
-      (let
-        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
-        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
-        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
-        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
-(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
-      in
-        SOME thm
-      end
-      handle _ => NONE
-      )
-  | _ => NONE
-  end
-*}
-
-ML {*
-fun bex_reg_eqv_simproc ss redex =
-  let
-    val ctxt = Simplifier.the_context ss
-    val thy = ProofContext.theory_of ctxt
-  in
-  case redex of
-      (ogl as ((Const (@{const_name "Bex"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
-      (let
-        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
-        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
-        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
-        val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
-(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
-      in
-        SOME thm
-      end
-      handle _ => NONE
-      )
-  | _ => NONE
-  end
-*}
-
-ML {*
 fun prep_trm thy (x, (T, t)) =
   (cterm_of thy (Var (x, T)), cterm_of thy t)
 
@@ -658,7 +610,6 @@
 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
 
-(* does not work yet
 ML {*
 fun regularize_tac ctxt =
   let
@@ -667,14 +618,13 @@
     val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
     val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
     val thy = ProofContext.theory_of ctxt
-    val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
-    val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
-    val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv}
-                                 addsimprocs [simproc3, simproc4]
-                                 addSolver equiv_solver
-    * TODO: Make sure that there are no list_rel, pair_rel etc involved *
+    val simp_set = (mk_minimal_ss ctxt) 
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv}
+                       addsimprocs [simproc3, simproc4]
+                       addSolver equiv_solver
+    (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
   in
   ObjectLogic.full_atomize_tac THEN'
@@ -689,35 +639,6 @@
     simp_tac simp_set
   ])
   end
-*}*)
-
-ML {*
-fun regularize_tac ctxt =
-let
-  val pat1 = [@{term "Ball (Respects R) P"}];
-  val pat2 = [@{term "Bex (Respects R) P"}];
-  val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
-  val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
-  val thy = ProofContext.theory_of ctxt
-  val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
-  val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
-  val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
-  val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
-  val simp_ctxt = (mk_minimal_ss ctxt) addsimprocs [simproc1, simproc2, simproc3, simproc4] 
-  (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
-  val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
-in
-  ObjectLogic.full_atomize_tac THEN'
-  simp_tac simp_ctxt THEN'
-  REPEAT_ALL_NEW (FIRST' [
-     rtac @{thm ball_reg_right},
-     rtac @{thm bex_reg_left},
-     resolve_tac (Inductive.get_monos ctxt),
-     rtac @{thm ball_all_comm},
-     rtac @{thm bex_ex_comm},
-     resolve_tac eq_eqvs,
-     simp_tac simp_ctxt])
-end
 *}
 
 section {* Injections of rep and abses *}