# HG changeset patch
# User wenzelm
# Date 1329238448 -3600
# Node ID 3d0629a9ffca633e4644f735f914535b28e8de8a
# Parent  9b3f6767d1751b8067851bb11b412f73ef96c15d
elininated unused INTLEAVE;

diff -r 9b3f6767d175 -r 3d0629a9ffca src/Pure/tactical.ML
--- 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;