# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259072110 -3600
# Node ID 7a3d86050e72d0110bdabfb9a99200b5873d53ca
# Parent  07fb696efa3d357a610d25c3aa24324aa92da408
added a prepare_tac

diff -r 07fb696efa3d -r 7a3d86050e72 IntEx.thy
--- a/IntEx.thy	Tue Nov 24 14:19:54 2009 +0100
+++ b/IntEx.thy	Tue Nov 24 15:15:10 2009 +0100
@@ -187,7 +187,7 @@
 *}
 
 
-lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"
+lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})
 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
diff -r 07fb696efa3d -r 7a3d86050e72 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 14:19:54 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 15:15:10 2009 +0100
@@ -1528,6 +1528,25 @@
   end
 *}
 
+ML {*
+fun spec_frees_tac [] = []
+  | spec_frees_tac (x::xs) = 
+       let
+         val spec' =  Drule.instantiate' [SOME (ctyp_of_term x)] [NONE, SOME x] @{thm spec} 
+       in
+         (rtac spec')::(spec_frees_tac xs)
+       end
+*}  
+
+ML {*
+val prepare_tac = CSUBGOAL (fn (concl, i) =>
+    let
+      val vrs = Thm.add_cterm_frees concl []
+    in
+      EVERY' (ObjectLogic.full_atomize_tac::spec_frees_tac vrs) i
+    end)
+*}
+
 lemma procedure:
   assumes a: "A"
   and     b: "A \<Longrightarrow> B"
@@ -1552,20 +1571,23 @@
      SOME (cterm_of thy inj_goal)]
   @{thm procedure}
 end
-
-fun procedure_tac rthm =
+*}
+  
+ML {*
+fun procedure_tac rthm ctxt =
+  prepare_tac THEN'
   Subgoal.FOCUS (fn {context, concl, ...} =>
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
     in
       EVERY1 [rtac rule, rtac rthm']
-    end)
+    end) ctxt
 *}
 
-(* FIXME: allex_prs and lambda_prs can be one function *)
 
 ML {*
+(* FIXME: allex_prs and lambda_prs can be one function *)
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
   THEN' (quotient_tac quot);