--- a/IntEx.thy	Fri Nov 27 02:23:49 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 02:35:50 2009 +0100
@@ -174,7 +174,7 @@
 *)
 
 ML {*
-  mk_regularize_trm @{context} 
+  regularize_trm @{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}
@@ -182,11 +182,10 @@
 *}
 
 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 {* procedure_tac @{context} @{thm plus_assoc_pre} 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 *})
-apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
-done 
+oops
 
 
 (*