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