diff -r 3359033eff79 -r d1aa26ecfecd IntEx.thy
--- a/IntEx.thy	Sat Nov 28 05:47:13 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 05:49:16 2009 +0100
@@ -149,7 +149,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) *}
@@ -189,8 +189,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 *})
@@ -226,7 +226,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) *}