--- 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);