added capabilities to handle mutual inductions

--- a/src/HOL/Nominal/nominal_induct.ML	Tue Jan 16 08:12:09 2007 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue Jan 16 10:25:38 2007 +0100
@@ -29,23 +29,21 @@
 
 (* prepare rule *)
 
-(*conclusions: ?P avoiding_struct ... insts*)
 fun inst_mutual_rule ctxt insts avoiding rules =
   let
-    val (concls, rule) =
-      (case RuleCases.mutual_rule ctxt rules of
-        NONE => error "Failed to join given rules into one mutual rule"
-      | SOME res => res);
-    val (cases, consumes) = RuleCases.get rule;
+
+    val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
+    val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
+    val (cases, consumes) = RuleCases.get joined_rule;
 
     val l = length rules;
     val _ =
       if length insts = l then ()
       else error ("Bad number of instantiations for " ^ string_of_int l ^ " rules");
 
-    fun subst inst rule =
+    fun subst inst concl =
       let
-        val vars = InductAttrib.vars_of (Thm.concl_of rule);
+        val vars = InductAttrib.vars_of concl;
         val m = length vars and n = length inst;
         val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
         val P :: x :: ys = vars;
@@ -56,9 +54,11 @@
         List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
       end;
      val substs =
-       map2 subst insts rules |> List.concat |> distinct (op =)
+       map2 subst insts concls |> List.concat |> distinct (op =)
        |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
-  in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
+  in 
+    (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
+  end;
 
 fun rename_params_rule internal xs rule =
   let