--- 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;