# HG changeset patch # User wenzelm # Date 1256851791 -3600 # Node ID 0affc253597974a3754848e1f655b0d7e4c37e76 # Parent 7a1f597f454ee0c9cd0b40b6f545d05786547997# Parent cd53fa891be529abd2bf3a5bb5651418857540d5 merged diff -r 7a1f597f454e -r 0affc2535979 src/Pure/meta_simplifier.ML --- 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; diff -r 7a1f597f454e -r 0affc2535979 src/Pure/search.ML --- 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;