--- a/IntEx.thy	Mon Nov 23 23:09:03 2009 +0100
+++ b/IntEx.thy	Tue Nov 24 01:36:50 2009 +0100
@@ -169,9 +169,53 @@
 
 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
-ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *}
+ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} 
+         @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *}
+
+ML {*
+  mk_REGULARIZE_goal @{context} 
+    @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}
+    @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+lemma procedure: 
+  assumes a: "A"
+  and     b: "A \<Longrightarrow> B"
+  and     c: "B = C"
+  and     d: "C = D"
+  shows   "D"
+  using a b c d
+  by simp
 
+ML {* 
+fun procedure_inst ctxt rtrm qtrm =
+let
+  val thy = ProofContext.theory_of ctxt
+  val rtrm' = HOLogic.dest_Trueprop rtrm
+  val qtrm' = HOLogic.dest_Trueprop qtrm
+in
+  Drule.instantiate' [] 
+    [SOME (cterm_of thy rtrm'), 
+     SOME (cterm_of thy (Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm'))),
+     SOME (cterm_of thy (Syntax.check_term ctxt (inj_REPABS ctxt (rtrm', qtrm'))))] 
+  @{thm procedure}
+end
 
+fun procedure_tac rthm =
+  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)
+*}
+
+lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"
+apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})
+sorry
 
 
 (*

--- a/QuotMain.thy	Mon Nov 23 23:09:03 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 01:36:50 2009 +0100
@@ -1374,13 +1374,11 @@
 (* rep-abs injection *)
 
 ML {*
-(* FIXME: is this the right get_fun function for rep-abs injection *)
 fun mk_repabs lthy (T, T') trm = 
   Quotient_Def.get_fun repF lthy (T, T') 
-  $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
 *}
 
-ML {* length *}
 
 ML {*
 (* bound variables need to be treated properly,  *)