| changeset 20852 | edc3147ab164 |
| parent 19482 | 9f11af8f7ef9 |
| child 22025 | 7c5896919eb8 |
--- 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;