diff -r 2e1b6a8a0fdd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Divides.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -429,7 +429,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "-(y * k) = y * - k")
- apply (erule ssubst)
+ apply (simp only:)
  apply (erule div_mult_self1_is_id)
 apply simp
 done
@@ -438,8 +438,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
  apply simp
 apply simp
 done
diff -r 2e1b6a8a0fdd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/HOL.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -871,6 +871,7 @@
   Hypsubst.hypsubst_setup
   (*prevent substitution on bool*)
   #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  #> Context_Rules.addWrapper (fn tac => Hypsubst.thin_triv_tac false ORELSE' tac)
 end
 *}
 
diff -r 2e1b6a8a0fdd src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Int.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -542,7 +542,7 @@
 lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
 apply (cases x)
 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x="y - Suc x" in exI, arith)
+apply (rule_tac x="y - Suc xa" in exI, arith)
 done
 
 
diff -r 2e1b6a8a0fdd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -1116,7 +1116,7 @@
  apply (simp (no_asm))
  apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  apply (simp (no_asm_simp) add: add_assoc [symmetric])
- apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
  apply (simp add: diff_union_single_conv)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
@@ -1127,7 +1127,7 @@
  apply (rule conjI)
   apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (rule conjI)
-  apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
+  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
   apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
diff -r 2e1b6a8a0fdd src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Nat.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -1076,7 +1076,7 @@
     -- {* elimination of @{text -} on @{text nat} *}
 by (cases "a < b")
   (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
-    not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero)
+    not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
 
 lemma nat_diff_split_asm:
   "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
diff -r 2e1b6a8a0fdd src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Parity.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -66,9 +66,10 @@
   by presburger
 
 lemma even_times_anything: "even (x::int) ==> even (x * y)"
-  by algebra
+  by (simp add: int_even_iff_2_dvd)
 
-lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
+lemma anything_times_even: "even (y::int) ==> even (x * y)"
+  by (simp add: int_even_iff_2_dvd)
 
 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" 
   by (simp add: even_def zmod_zmult1_eq)
diff -r 2e1b6a8a0fdd src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Transcendental.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -1909,7 +1909,7 @@
 apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y")
 apply (rule_tac [2] IVT2)
 apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos)
-apply (cut_tac x = xa and y = y in linorder_less_linear)
+apply (cut_tac x = xa and y = ya in linorder_less_linear)
 apply (rule ccontr, auto)
 apply (drule_tac f = cos in Rolle)
 apply (drule_tac [5] f = cos in Rolle)
@@ -2184,9 +2184,9 @@
 
 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
 apply (cut_tac y = y in lemma_tan_total1, auto)
-apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
-apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
-apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
+apply (cut_tac x = xa and y = ya in linorder_less_linear, auto)
+apply (subgoal_tac [2] "\<exists>z. ya < z & z < xa & DERIV tan z :> 0")
+apply (subgoal_tac "\<exists>z. xa < z & z < ya & DERIV tan z :> 0")
 apply (rule_tac [4] Rolle)
 apply (rule_tac [2] Rolle)
 apply (auto intro!: DERIV_tan DERIV_isCont exI 
diff -r 2e1b6a8a0fdd src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Word/BinBoolList.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -570,7 +570,7 @@
 
 lemma takefill_same': 
   "l = length xs ==> takefill fill l xs = xs"
-  by clarify (induct xs, auto)
+  by (induct xs arbitrary: l, auto)
  
 lemmas takefill_same [simp] = takefill_same' [OF refl]
 
diff -r 2e1b6a8a0fdd src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Word/TdThs.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -197,7 +197,7 @@
    prefer 2
    apply (simp add: o_assoc [symmetric])
   apply (rule ext)
-  apply (drule fun_cong)
+  apply (drule_tac f="?a o ?b" in fun_cong)
   apply simp
   done
 
diff -r 2e1b6a8a0fdd src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Word/WordShift.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -394,7 +394,7 @@
   "us = of_bl bl >> n ==> length bl <= size us --> 
    us = of_bl (take (length bl - n) bl)"
   apply (unfold shiftr_def)
-  apply hypsubst
+  apply hypsubst_thin
   apply (unfold word_size)
   apply (induct n)
    apply clarsimp
@@ -428,6 +428,7 @@
   apply clarsimp
   apply (case_tac x, force)
   apply (case_tac m, auto)
+  apply hypsubst_thin
   apply (drule sym)
   apply auto
   apply (induct_tac list, auto)
@@ -442,6 +443,7 @@
   apply clarsimp
   apply (case_tac x, force)
   apply (case_tac m, auto)
+  apply hypsubst_thin
   apply (drule sym)
   apply auto
   apply (induct_tac list, auto)
@@ -934,6 +936,7 @@
   apply safe
    defer
    apply (clarsimp split: prod.splits)
+   apply hypsubst_thin
    apply (drule word_ubin.norm_Rep [THEN ssubst])
    apply (drule split_bintrunc)
    apply (simp add : of_bl_def bl2bin_drop word_size
diff -r 2e1b6a8a0fdd src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/ex/Dedekind_Real.thy	Mon Aug 23 17:33:59 2010 +1000
@@ -307,7 +307,7 @@
      "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
 apply (auto simp add: add_set_def)
 apply (frule preal_exists_greater [of A], auto) 
-apply (rule_tac x="u + y" in exI)
+apply (rule_tac x="u + ya" in exI)
 apply (auto intro: add_strict_left_mono)
 done
 
@@ -434,7 +434,7 @@
      "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
 apply (auto simp add: mult_set_def)
 apply (frule preal_exists_greater [of A], auto) 
-apply (rule_tac x="u * y" in exI)
+apply (rule_tac x="u * ya" in exI)
 apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
                    mult_strict_right_mono)
 done
@@ -1583,7 +1583,7 @@
       "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
 apply (simp add: real_of_preal_def real_zero_def, cases x)
 apply (auto simp add: real_minus add_ac)
-apply (cut_tac x = x and y = y in linorder_less_linear)
+apply (cut_tac x = xa and y = y in linorder_less_linear)
 apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric])
 done
 
diff -r 2e1b6a8a0fdd src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Jul 28 06:38:17 2010 +1000
+++ b/src/Provers/hypsubst.ML	Mon Aug 23 17:33:59 2010 +1000
@@ -54,6 +54,7 @@
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
+  val thin_triv_tac          : bool -> int -> tactic
 end;
 
 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
@@ -115,27 +116,55 @@
      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
                        then raise Match
                        else false               (*eliminates u*)
-     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
+     | (Free f, _) =>  if bnd orelse Logic.occs(Free f,u) orelse
                           novars andalso has_vars u
                        then raise Match
                        else true                (*eliminates t*)
-     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
+     | (_, Free f) =>  if bnd orelse Logic.occs(Free f,t) orelse
                           novars andalso has_vars t
                        then raise Match
                        else false               (*eliminates u*)
      | _ => raise Match;
 
+(* Counts the occurences of Free and Bound variables in a term. *)
+fun count_vars' _ (Free f) = Termtab.map_default (Free f, 0) (fn x => x + 1)
+  | count_vars' _ (Var _) = I
+  | count_vars' _ (Const _) = I
+  | count_vars' n (Bound m) = Termtab.map_default (Bound (m - n), 0)
+      (fn x => x + 1)
+  | count_vars' n (Abs (_, _, t)) = count_vars' (n + 1) t
+  | count_vars' n (f $ x) = count_vars' n f o count_vars' n x
+
+fun count_vars ts = fold (count_vars' 0) ts Termtab.empty
+
+(* An equality hypothesis 'x = y' is trivial if substituting with it would have
+   no useful effect. The principal test for this is if x or y is a unique
+   variable, occuring nowhere else in the goal.  The exception to the rule is
+   if x is bound and y is unique but free. *)
+fun triv_asm bnd t = let
+    val vars = count_vars (Logic.strip_assums_concl t
+        :: Logic.strip_assums_hyp t)
+    fun triv v = (if bnd then is_Bound v else true) 
+      andalso (Termtab.lookup vars v = SOME 1)
+  in fn eq => case try (pairself Envir.beta_eta_contract
+            o Data.dest_eq o Data.dest_Trueprop) eq of
+      NONE => false
+    | SOME (a, b) => if exists is_Bound [a, b]
+        then exists triv (filter is_Bound [a, b])
+        else exists triv [a, b]
+  end
+
 (*Locates a substitutable variable on the left (resp. right) of an equality
    assumption.  Returns the number of intervening assumptions. *)
-fun eq_var bnd novars =
-  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
-        | eq_var_aux k (Const("==>",_) $ A $ B) =
-              ((k, inspect_pair bnd novars
-                    (Data.dest_eq (Data.dest_Trueprop A)))
-               handle TERM _ => eq_var_aux (k+1) B
-                 | Match => eq_var_aux (k+1) B)
-        | eq_var_aux k _ = raise EQ_VAR
-  in  eq_var_aux 0  end;
+fun eq_var bnd novars skiptriv t = let
+    val triv = if skiptriv then triv_asm false t else K false
+    fun eq_var_aux hyp =
+      (if (inspect_pair bnd novars (Data.dest_eq (Data.dest_Trueprop hyp)))
+      then if triv hyp then NONE else SOME true
+      else SOME false)
+        handle TERM _ => NONE | Match => NONE
+  in get_index eq_var_aux (Logic.strip_assums_hyp t) |> the
+    handle Option => raise EQ_VAR end
 
 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   No vars are allowed here, as simpsets are built from meta-assumptions*)
@@ -154,11 +183,12 @@
   fun gen_hyp_subst_tac bnd =
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
-        val (k, _) = eq_var bnd true Bi
+        val (k, symopt) = eq_var bnd true true Bi
         val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
           setmksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
-        etac thin_rl i, rotate_tac (~k) i]
+        if not symopt then dtac Data.sym i THEN rotate_tac (~1) i else all_tac,
+        rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
     in REPEAT_DETERM1 o tac end;
 
@@ -201,28 +231,41 @@
 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
 (* premises containing meta-implications or quantifiers                *)
 
+(* copied from blast.ML *)
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+
+val dup_subst = rev_dup_elim ssubst
+
 (*Old version of the tactic above -- slower but the only way
   to handle equalities containing Vars.*)
 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
       let val n = length(Logic.strip_assums_hyp Bi) - 1
-          val (k,symopt) = eq_var bnd false Bi
+          val (k,symopt) = eq_var bnd false true Bi
+          val rl = if symopt then dup_subst else (Data.sym RS dup_subst)
       in
          DETERM
            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
                    rotate_tac 1 i,
                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
-                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
+                   inst_subst_tac symopt rl i,
                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
       end
       handle THM _ => no_tac | EQ_VAR => no_tac);
 
-(*Substitutes for Free or Bound variables*)
-val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
-        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
+fun thin_triv_tac bnd = SUBGOAL (fn (t, i) => let
+    val n = find_index (triv_asm bnd t) (Logic.strip_assums_hyp t)
+  in if n <> ~1 then EVERY' 
+    [rotate_tac n, etac thin_rl, rotate_tac (~ n)] i else no_tac end)
+
+(*Substitutes for Free or Bound variables, thins out Bound equalities *)
+val hyp_subst_tac = REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
+        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false,
+        thin_triv_tac true];
 
 (*Substitutes for Bound variables only -- this is always safe*)
 val bound_hyp_subst_tac =
-    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
+    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true
+      ORELSE' thin_triv_tac true;
 
 
 (** Version for Blast_tac.  Hyps that are affected by the substitution are
@@ -256,7 +299,7 @@
 
 
 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
-      let val (k,symopt) = eq_var false false Bi
+      let val (k,symopt) = eq_var false false false Bi
           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
           (*omit selected equality, returning other hyps*)
           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
@@ -282,10 +325,15 @@
 
 (* theory setup *)
 
+val hypsubst_thin = REPEAT_DETERM1 o (hyp_subst_tac ORELSE' thin_triv_tac false)
+
 val hypsubst_setup =
   Method.setup @{binding hypsubst}
     (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
     "substitution using an assumption (improper)" #>
+  Method.setup @{binding hypsubst_thin}
+    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hypsubst_thin))))
+    "substitution and discarding of an assumption (improper)" #>
   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
     "simple substitution";
 
