diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -7,7 +7,7 @@
 sig
   val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     (string * typ) list -> (string * typ) list list -> thm list ->
-    thm list -> int -> RuleCases.cases_tactic
+    thm list -> int -> Rule_Cases.cases_tactic
   val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 struct
@@ -31,9 +31,9 @@
 
 fun inst_mutual_rule ctxt insts avoiding rules =
   let
-    val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
+    val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules;
     val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
-    val (cases, consumes) = RuleCases.get joined_rule;
+    val (cases, consumes) = Rule_Cases.get joined_rule;
 
     val l = length rules;
     val _ =
@@ -93,12 +93,12 @@
       split_all_tuples
       #> rename_params_rule true
         (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
-    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
+    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
   in
     (fn i => fn st =>
       rules
       |> inst_mutual_rule ctxt insts avoiding
-      |> RuleCases.consume (flat defs) facts
+      |> Rule_Cases.consume (flat defs) facts
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS