--- a/IntEx.thy	Sat Nov 28 04:02:54 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 05:29:30 2009 +0100
@@ -151,7 +151,7 @@
 
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
@@ -191,8 +191,8 @@
 
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
@@ -228,7 +228,7 @@
 
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}