tuned

--- a/src/Pure/search.ML	Wed Oct 04 11:18:39 2006 +0200
+++ b/src/Pure/search.ML	Wed Oct 04 11:50:37 2006 +0200
@@ -67,7 +67,7 @@
 		then SOME(st, Seq.make
 			         (fn()=> depth (st::used) (stq::qs)))
 		else depth used (tac st :: stq :: qs)
-  in  traced_tac (fn st => depth [] ([Seq.single st]))  end;
+  in  traced_tac (fn st => depth [] [Seq.single st])  end;