eliminanated some unreferenced identifiers;
tuned;

--- a/src/Pure/Isar/overloading.ML	Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Apr 26 20:30:50 2010 +0200
@@ -67,8 +67,8 @@
 
 fun improve_term_check ts ctxt =
   let
-    val { primary_constraints, secondary_constraints, improve, subst,
-      consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt;
+    val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
+      ImprovableSyntax.get ctxt;
     val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
     val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
     val passed_or_abbrev = passed orelse is_abbrev;

--- a/src/Pure/Isar/proof.ML	Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Apr 26 20:30:50 2010 +0200
@@ -792,7 +792,7 @@
 
 fun implicit_vars props =
   let
-    val (var_props, props') = take_prefix is_var props;
+    val (var_props, _) = take_prefix is_var props;
     val explicit_vars = fold Term.add_vars var_props [];
     val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
   in map (Logic.mk_term o Var) vars end;
@@ -845,11 +845,10 @@
 
 fun generic_qed after_ctxt state =
   let
-    val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state;
+    val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
     val outer_state = state |> close_block;
     val outer_ctxt = context_of outer_state;
 
-    val ((_, pos), stmt, _) = statement;
     val props =
       flat (tl stmt)
       |> Variable.exportT_terms goal_ctxt outer_ctxt;

--- a/src/Pure/Isar/rule_cases.ML	Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Mon Apr 26 20:30:50 2010 +0200
@@ -368,7 +368,7 @@
         map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
       in Logic.list_rename_params (xs, prem) end;
     fun rename_prems prop =
-      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
+      let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;
   in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
 

--- a/src/Pure/meta_simplifier.ML	Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Apr 26 20:30:50 2010 +0200
@@ -834,7 +834,6 @@
   in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
   handle THM _ =>
     let
-      val thy = Thm.theory_of_thm thm;
       val _ $ _ $ prop0 = Thm.prop_of thm;
     in
       trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';

--- a/src/Pure/tactic.ML	Mon Apr 26 16:08:04 2010 +0200
+++ b/src/Pure/tactic.ML	Mon Apr 26 20:30:50 2010 +0200
@@ -188,9 +188,6 @@
   let val (_, _, Bi, _) = dest_state (st, i)
   in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
 
-(*params of subgoal i as they are printed*)
-fun params_of_state i st = rev (innermost_params i st);
-
 
 (*** Applications of cut_rl ***)