# HG changeset patch # User wenzelm # Date 1136477648 -3600 # Node ID 6538fdcc98dcac77b76cfcabef50f6ad0d549d5e # Parent 4fdd39ea2f409042632cb0a71f4e3c4094405354 added strict_mutual_rule; diff -r 4fdd39ea2f40 -r 6538fdcc98dc src/Pure/Isar/rule_cases.ML --- 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;