merged

--- a/src/Pure/meta_simplifier.ML	Thu Oct 29 22:16:58 2009 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Oct 29 22:29:51 2009 +0100
@@ -1025,7 +1025,7 @@
                  val b' = #1 (Term.dest_Free (Thm.term_of v));
                  val _ =
                    if b <> b' then
-                     warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
+                     tracing ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
                    else ();
                  val ss' = add_bound ((b', T), a) ss;
                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;

--- a/src/Pure/search.ML	Thu Oct 29 22:16:58 2009 +0100
+++ b/src/Pure/search.ML	Thu Oct 29 22:29:51 2009 +0100
@@ -21,6 +21,7 @@
   val iter_deepen_limit: int Unsynchronized.ref
   val THEN_ITER_DEEPEN: tactic -> (thm -> bool) -> (int -> tactic) -> tactic
   val ITER_DEEPEN: (thm -> bool) -> (int -> tactic) -> tactic
+  val trace_DEEPEN: bool Unsynchronized.ref
   val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic
   val trace_BEST_FIRST: bool Unsynchronized.ref
   val THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic
@@ -174,13 +175,15 @@
 
 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   using increment "inc" up to limit "lim". *)
+val trace_DEEPEN = Unsynchronized.ref false;
+
 fun DEEPEN (inc,lim) tacf m i =
   let fun dpn m st =
        st |> (if has_fewer_prems i st then no_tac
               else if m>lim then
-                       (warning "Search depth limit exceeded: giving up";
+                       (tracing "Search depth limit exceeded: giving up";
                         no_tac)
-              else (priority ("Search depth = " ^ string_of_int m);
+              else (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else ();
                              tacf m i  ORELSE  dpn (m+inc)))
   in  dpn m  end;