added strict_mutual_rule;

--- a/src/Pure/Isar/rule_cases.ML	Thu Jan 05 17:14:07 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Jan 05 17:14:08 2006 +0100
@@ -37,6 +37,7 @@
   val rename_params: string list list -> thm -> thm
   val params: string list list -> 'a attribute
   val mutual_rule: thm list -> (int list * thm) option
+  val strict_mutual_rule: thm list -> int list * thm
 end;
 
 structure RuleCases: RULE_CASES =
@@ -301,6 +302,11 @@
 
 end;
 
+fun strict_mutual_rule ths =
+  (case mutual_rule ths of
+    NONE => error "Failed to join given rules into one mutual rule"
+  | SOME res => res);
+
 end;
 
 structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;