--- a/QuotMain.thy	Fri Dec 04 14:11:20 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 14:35:36 2009 +0100
@@ -776,58 +776,6 @@
   end
 *}
 
-ML {*
-val APPLY_RSP_TAC =
-  Subgoal.FOCUS (fn {concl, asms, context,...} =>
-    case ((HOLogic.dest_Trueprop (term_of concl))) of
-       ((R2 $ (f $ x) $ (g $ y))) =>
-          let
-            val (asmf, asma) = find_qt_asm (map term_of asms);
-          in
-            if (fastype_of asmf) = (fastype_of f) then no_tac else let
-              val ty_a = fastype_of x;
-              val ty_b = fastype_of asma;
-              val ty_c = range_type (type_of f);
-              val ty_d = range_type (type_of asmf);
-              val thy = ProofContext.theory_of context;
-              val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d];
-              val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
-              val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
-              val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
-              val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm))
-            in
-              rtac thm 1
-            end
-          end
-     | _ => no_tac)
-*}
-
-ML {*
-val APPLY_RSP1_TAC =
-  Subgoal.FOCUS (fn {concl, asms, context,...} =>
-    case ((HOLogic.dest_Trueprop (term_of concl))) of
-       ((R2 $ (f $ x) $ (g $ y))) =>
-          let
-            val (asmf, asma) = find_qt_asm (map term_of asms);
-          in
-            if (fastype_of asmf) = (fastype_of f) then no_tac else let
-              val ty_a = fastype_of x;
-              val ty_b = fastype_of asma;
-              val ty_c = range_type (type_of f);
-(*              val ty_d = range_type (type_of asmf);*)
-              val thy = ProofContext.theory_of context;
-              val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c];
-              val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
-              val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y];
-              val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1}
-              (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
-            in
-              rtac thm 1
-            end
-          end
-     | _ => no_tac)
-*}
-
 (* It proves the QUOTIENT assumptions by calling quotient_tac *)
 ML {*
 fun solve_quotient_assum i ctxt thm =
@@ -851,7 +799,7 @@
 *}
 
 ML {*
-val APPLY_RSP1_TAC' =
+val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
     case ((HOLogic.dest_Trueprop (term_of concl))) of
       ((R2 $ (f $ x) $ (g $ y))) =>
@@ -864,7 +812,7 @@
             val ty_c = range_type (type_of f);
             val thy = ProofContext.theory_of context;
             val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
-            val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1}
+            val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
             val te = solve_quotient_assums context thm
             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
             val thm = Drule.instantiate' [] t_inst te
@@ -1027,8 +975,8 @@
 fun inj_repabs_tac ctxt rel_refl trans2 =
   (FIRST' [
     inj_repabs_tac_match ctxt trans2,
-    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN'
+    (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
+    NDT ctxt "A" (apply_rsp_tac ctxt THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
@@ -1055,15 +1003,6 @@
 
 section {* Cleaning of the theorem *}
 
-
-(* TODO: This is slow *)
-(*
-ML {*
-fun allex_prs_tac ctxt =
-  (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
-*}
-*)
-
 ML {*
 fun make_inst lhs t =
   let
@@ -1089,7 +1028,7 @@
     val thy = ProofContext.theory_of ctxt;
     val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
     val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-    val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
+    val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
     val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
     val tl = Thm.lhs_of ts;
@@ -1140,10 +1079,10 @@
  Cleaning the theorem consists of 6 kinds of rewrites.
  The first two need to be done before fun_map is unfolded
 
- - LAMBDA_PRS:
+ - lambda_prs:
      (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
 
- - FORALL_PRS (and the same for exists: EXISTS_PRS)
+ - all_prs (and the same for exists: ex_prs)
      \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f
 
  - Rewriting with definitions from the argument defs
@@ -1300,7 +1239,7 @@
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
       val quotients = quotient_rules_get lthy
-      val trans2 = map (fn x => @{thm EQUALS_RSP} OF [x]) quotients
+      val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
       val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
     in
       EVERY1