elininated unused INTLEAVE;

--- a/src/Pure/tactical.ML	Tue Feb 14 17:51:29 2012 +0100
+++ b/src/Pure/tactical.ML	Tue Feb 14 17:54:08 2012 +0100
@@ -5,7 +5,7 @@
 *)
 
 infix 1 THEN THEN' THEN_ALL_NEW;
-infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
+infix 0 ORELSE APPEND ORELSE' APPEND';
 infix 0 THEN_ELSE;
 
 signature TACTICAL =
@@ -14,12 +14,10 @@
   val THEN: tactic * tactic -> tactic
   val ORELSE: tactic * tactic -> tactic
   val APPEND: tactic * tactic -> tactic
-  val INTLEAVE: tactic * tactic -> tactic
   val THEN_ELSE: tactic * (tactic*tactic) -> tactic
   val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val all_tac: tactic
   val no_tac: tactic
   val DETERM: tactic -> tactic
@@ -100,11 +98,6 @@
 fun (tac1 APPEND tac2) st =
   Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
 
-(*Like APPEND, but interleaves results of tac1 and tac2.*)
-fun (tac1 INTLEAVE tac2) st =
-    Seq.interleave(tac1 st,
-                        Seq.make(fn()=> Seq.pull (tac2 st)));
-
 (*Conditional tactic.
         tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
         tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
@@ -120,7 +113,6 @@
 fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;
 fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;
 fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x;
-fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
 
 (*passes all proofs through unchanged;  identity of THEN*)
 fun all_tac st = Seq.single st;