--- a/src/HOL/Hyperreal/HSeries.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy Mon Oct 09 02:19:51 2006 +0200
@@ -83,7 +83,7 @@
done
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
-by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
+by (drule_tac f = f in sumhr_split_add [symmetric], simp)
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
apply (cases n, cases m)
--- a/src/HOL/Hyperreal/HTranscendental.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Mon Oct 09 02:19:51 2006 +0200
@@ -71,7 +71,7 @@
lemma hypreal_inverse_sqrt_pow2:
"0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
-apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
+apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric])
apply (auto dest: hypreal_sqrt_gt_zero_pow2)
done
--- a/src/HOL/Hyperreal/NthRoot.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy Mon Oct 09 02:19:51 2006 +0200
@@ -358,7 +358,7 @@
done
lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
-by (cut_tac n1 = 2 and a1 = "sqrt x" in power_inverse [symmetric], auto)
+by (cut_tac n = 2 and a = "sqrt x" in power_inverse [symmetric], auto)
lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
apply (drule real_le_imp_less_or_eq)
--- a/src/HOL/Hyperreal/Poly.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Mon Oct 09 02:19:51 2006 +0200
@@ -964,7 +964,7 @@
apply (simp add: rsquarefree_def, safe)
apply (frule_tac a = a in order_decomp)
apply (drule_tac x = a in spec)
-apply (drule_tac a1 = a in order_root2 [symmetric])
+apply (drule_tac a = a in order_root2 [symmetric])
apply (auto simp del: pmult_Cons)
apply (rule_tac x = q in exI, safe)
apply (simp add: poly_mult fun_eq)
--- a/src/HOL/NumberTheory/Gauss.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Mon Oct 09 02:19:51 2006 +0200
@@ -308,7 +308,7 @@
lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
apply (auto simp add: C_def)
apply (insert finite_B SR_B_inj)
- apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id [symmetric], auto)
+ apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto)
apply (rule setprod_same_function_zcong)
apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
done
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Mon Oct 09 02:19:51 2006 +0200
@@ -604,7 +604,7 @@
nat(setsum (%x. ((x * q) div p)) P_set) =
nat((setsum (%x. ((x * p) div q)) Q_set) +
(setsum (%x. ((x * q) div p)) P_set))"
- apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
+ apply (rule_tac z = "setsum (%x. ((x * p) div q)) Q_set" in
nat_add_distrib [symmetric])
apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric])
done
--- a/src/Pure/Isar/calculation.ML Mon Oct 09 02:19:49 2006 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Oct 09 02:19:51 2006 +0200
@@ -85,7 +85,7 @@
val symmetric = Thm.rule_attribute (fn x => fn th =>
(case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
- ([th'], _) => th'
+ ([th'], _) => Drule.zero_var_indexes th'
| ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
| _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
--- a/src/ZF/Induct/Multiset.thy Mon Oct 09 02:19:49 2006 +0200
+++ b/src/ZF/Induct/Multiset.thy Mon Oct 09 02:19:51 2006 +0200
@@ -637,8 +637,8 @@
shows "P(M)"
apply (rule multiset_induct2 [OF M])
apply (simp_all add: P0)
-apply (frule_tac [2] a1 = b in munion_single_case2 [symmetric])
-apply (frule_tac a1 = a in munion_single_case1 [symmetric])
+apply (frule_tac [2] a = b in munion_single_case2 [symmetric])
+apply (frule_tac a = a in munion_single_case1 [symmetric])
apply (auto intro: step)
done