# HG changeset patch
# User webertj
# Date 1159955437 -7200
# Node ID edc3147ab164f8a1e92be51a4aa2ee3335dc4440
# Parent  bf80cb83f8be366c245f77d9c8e3bb84d8847023
tuned

diff -r bf80cb83f8be -r edc3147ab164 src/Pure/search.ML
--- 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;