src/Pure/tctical.ML
changeset 19861 620d90091788
parent 19646 91c0ae7e542b
child 20194 c9dbce9a23a1
     1.1 --- a/src/Pure/tctical.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Pure/tctical.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -102,8 +102,7 @@
     1.4    Like ORELSE, but allows backtracking on both tac1 and tac2.
     1.5    The tactic tac2 is not applied until needed.*)
     1.6  fun (tac1 APPEND tac2) st =
     1.7 -  Seq.append(tac1 st,
     1.8 -                  Seq.make(fn()=> Seq.pull (tac2 st)));
     1.9 +  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
    1.10  
    1.11  (*Like APPEND, but interleaves results of tac1 and tac2.*)
    1.12  fun (tac1 INTLEAVE tac2) st =