--- a/IntEx2.thy	Sun Dec 06 11:39:34 2009 +0100
+++ b/IntEx2.thy	Sun Dec 06 13:41:42 2009 +0100
@@ -171,16 +171,16 @@
   fix i j k :: int
   show "(i + j) + k = i + (j + k)"
     unfolding add_int_def
-    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})
     done
   show "i + j = j + i" 
     unfolding add_int_def
-    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
     done
   show "0 + i = (i::int)"
     unfolding add_int_def Zero_int_def 
     apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* regularize_tac @{context} 1 *})
     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
     defer
     apply(tactic {* clean_tac @{context} 1*})
@@ -188,7 +188,7 @@
   show "- i + i = 0"
     unfolding add_int_def minus_int_def Zero_int_def 
     apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* regularize_tac @{context} 1 *})
     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
     defer
     apply(tactic {* clean_tac @{context} 1*})
@@ -198,7 +198,7 @@
   show "(i * j) * k = i * (j * k)"
     unfolding mult_int_def 
     apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* regularize_tac @{context} 1 *})
     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
     defer
     apply(tactic {* clean_tac @{context} 1*})
@@ -206,7 +206,7 @@
   show "i * j = j * i"
     unfolding mult_int_def 
     apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* regularize_tac @{context} 1 *})
     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
     defer
     apply(tactic {* clean_tac @{context} 1*})
@@ -214,7 +214,7 @@
   show "1 * i = i"
     unfolding mult_int_def One_int_def
     apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* regularize_tac @{context} 1 *})
     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
     defer
     apply(tactic {* clean_tac @{context} 1*})
@@ -222,7 +222,7 @@
   show "(i + j) * k = i * k + j * k"
     unfolding mult_int_def add_int_def
     apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* regularize_tac @{context} 1 *})
     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
     defer
     apply(tactic {* clean_tac @{context} 1*})
@@ -269,21 +269,21 @@
   fix i j k :: int
   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})
     done
   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
     by (auto simp add: less_int_def dest: antisym) 
   show "i \<le> i"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})
     done
   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})
     done
   show "i \<le> j \<or> j \<le> i"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
     done
 qed
 
@@ -312,7 +312,7 @@
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
     unfolding le_int_def add_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})
     done
 qed