| author | aspinall | 
| Wed, 18 Jul 2007 14:46:59 +0200 | |
| changeset 23841 | 598839baafed | 
| parent 23840 | 0295493ba748 | 
| child 23842 | 9d87177f1f89 | 
--- a/src/Pure/search.ML Wed Jul 18 14:44:49 2007 +0200 +++ b/src/Pure/search.ML Wed Jul 18 14:46:59 2007 +0200 @@ -196,7 +196,7 @@ else if m>lim then (warning "Search depth limit exceeded: giving up"; no_tac) - else (warning ("Search depth = " ^ string_of_int m); + else (priority ("Search depth = " ^ string_of_int m); tacf m i ORELSE dpn (m+inc))) in dpn m end;