diff -r ec44df8ffd21 -r cb53a778455e src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Nov 16 17:45:33 2005 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Nov 16 17:45:34 2005 +0100
@@ -5,6 +5,8 @@
 Manage local contexts of rules.
 *)
 
+infix 1 THEN_ALL_NEW_CASES;
+
 signature RULE_CASES =
 sig
   val consumes: int -> 'a attribute
@@ -22,6 +24,7 @@
   val params: string list list -> 'a attribute
   type tactic
   val NO_CASES: Tactical.tactic -> tactic
+  val THEN_ALL_NEW_CASES: (int -> tactic) * (int -> Tactical.tactic) -> int -> tactic
 end;
 
 structure RuleCases: RULE_CASES =
@@ -96,8 +99,7 @@
   assumes: (string * term list) list,
   binds: (indexname * term option) list};
 
-val strip_params =
-  Logic.strip_params #> map (fn (x, T) => (the_default x (try Syntax.dest_skolem x), T));
+val strip_params = map (apfst Syntax.deskolem) o Logic.strip_params;
 
 fun prep_case is_open thy (split, raw_prop) name =
   let
@@ -156,6 +158,12 @@
 
 fun NO_CASES tac = Seq.map (rpair []) o tac;
 
+fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
+  st |> tac1 i |> Seq.maps (fn (st', cases) =>
+    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'));
+
 end;
 
 val NO_CASES = RuleCases.NO_CASES;
+val op THEN_ALL_NEW_CASES = RuleCases.THEN_ALL_NEW_CASES;
+