# HG changeset patch
# User wenzelm
# Date 1136477647 -3600
# Node ID 4fdd39ea2f409042632cb0a71f4e3c4094405354
# Parent  002d371401f58bc018d8cdd76f0fd9524301297b
RuleCases.strict_mutual_rule;
export internalize;

diff -r 002d371401f5 -r 4fdd39ea2f40 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Thu Jan 05 12:09:26 2006 +0100
+++ b/src/Provers/induct_method.ML	Thu Jan 05 17:14:07 2006 +0100
@@ -23,6 +23,7 @@
   val inner_atomize_tac: int -> tactic
   val rulified_term: thm -> theory * term
   val rulify_tac: int -> tactic
+  val internalize: int -> thm -> thm
   val guess_instance: thm -> int -> thm -> thm Seq.seq
   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
@@ -205,11 +206,6 @@
 fun rule_instance thy inst rule =
   Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
 
-fun mutual_rule ths =
-  (case RuleCases.mutual_rule ths of
-    NONE => error "Failed to join given rules into one mutual rule"
-  | SOME res => res);
-
 fun internalize k th =
   th |> Thm.permute_prems 0 k
   |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm);
@@ -394,7 +390,7 @@
 
     val ruleq =
       (case opt_rule of
-        SOME rs => Seq.single (inst_rule (mutual_rule rs))
+        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule rs))
       | NONE =>
           (find_inductS ctxt facts @
             map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))