eliminated dead code;
tuned;

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -95,7 +95,6 @@
 );
 
 fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
 fun update_thread xs = AList.update Thread.equal xs;
 
 
@@ -121,7 +120,8 @@
 (* unregister thread *)
 
 fun unregister (success, message) thread = Synchronized.change state
-  (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+  (fn state as
+      State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
       SOME (birthtime, _, description) =>
         let
@@ -326,9 +326,11 @@
 fun print_provers thy = Pretty.writeln
   (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
 
-fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
-  NONE => NONE
-| SOME (prover, _) => SOME prover;
+fun get_prover name thy =
+  (case Symtab.lookup (Provers.get thy) name of
+    NONE => NONE
+  | SOME (prover, _) => SOME prover);
+
 
 (* start prover thread *)
 

--- a/src/HOL/Tools/lin_arith.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -767,8 +767,6 @@
 
 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
 
-val map_data = Fast_Arith.map_data;
-
 fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
     lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};

--- a/src/HOL/Tools/old_primrec.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -318,31 +318,7 @@
 val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
 val add_primrec_i = gen_primrec_i thy_note (thy_def false);
 val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
-fun gen_primrec note def alt_name specs =
-  gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
 
 end;
 
-
-(* see primrec.ML (* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_unchecked_name =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
-      P.name >> pair false) --| P.$$$ ")")) (false, "");
-
-val primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-
-val _ =
-  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
-      Toplevel.theory (snd o
-        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
-          (map P.triple_swap eqns))));
-
-end;*)
-
 end;

--- a/src/HOL/Tools/recdef.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/recdef.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -47,11 +47,6 @@
 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
 
-fun pretty_hints ({simps, congs, wfs}: hints) =
- [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
-  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
-  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
-
 
 (* congruence rules *)
 

--- a/src/Provers/classical.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/Provers/classical.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -768,7 +768,7 @@
 (*Non-deterministic!  Could always expand the first unsafe connective.
   That's hard to implement and did not perform better in experiments, due to
   greater search depth required.*)
-fun dup_step_tac (cs as (CS{dup_netpair,...})) =
+fun dup_step_tac (CS {dup_netpair, ...}) =
   biresolve_from_nets_tac dup_netpair;
 
 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)

--- a/src/Tools/induct_tacs.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/Tools/induct_tacs.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -28,7 +28,7 @@
 
 fun gen_case_tac ctxt0 s opt_rule i st =
   let
-    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
+    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
       (case opt_rule of
         SOME rule => rule