--- a/LFex.thy	Fri Nov 27 04:02:20 2009 +0100
+++ b/LFex.thy	Fri Nov 27 07:00:14 2009 +0100
@@ -263,8 +263,7 @@
     val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
   in
   (ObjectLogic.full_atomize_tac) THEN'
-  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) 
-  THEN'
+  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN'
   REPEAT_ALL_NEW (FIRST' [
     (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
     (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
@@ -274,7 +273,8 @@
     (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
     (resolve_tac (Inductive.get_monos ctxt)),
     rtac @{thm move_forall},
-    rtac @{thm move_exists}
+    rtac @{thm move_exists},
+    (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
   ])
   end
 *}
@@ -300,95 +300,9 @@
    ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *})
-apply(atomize (full))
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule test)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule test)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule test)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-
-
-thm test[OF mp]
-
-
 prefer 2
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(thin_tac "Respects (akind ===> akind ===> op =) x") 
-apply(thin_tac "Respects (aty ===> aty ===> op =) xa")
-apply(thin_tac "Respects (atrm ===> atrm ===> op =) xb")
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(rule conjI)
-prefer 2
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-using al_refl
-apply(simp add: Respects_def)
-
-
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-apply(rule Set.imp_mono)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-apply(rule Set.imp_mono)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-apply(rule impI) apply(assumption)
+apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *})
 
 ML {*
 val rty_qty_rel =