RuleCases.strict_mutual_rule;
authorwenzelm
Thu Jan 05 17:14:07 2006 +0100 (2006-01-05)
changeset 185804fdd39ea2f40
parent 18579 002d371401f5
child 18581 6538fdcc98dc
RuleCases.strict_mutual_rule;
export internalize;
src/Provers/induct_method.ML
     1.1 --- a/src/Provers/induct_method.ML	Thu Jan 05 12:09:26 2006 +0100
     1.2 +++ b/src/Provers/induct_method.ML	Thu Jan 05 17:14:07 2006 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    val inner_atomize_tac: int -> tactic
     1.5    val rulified_term: thm -> theory * term
     1.6    val rulify_tac: int -> tactic
     1.7 +  val internalize: int -> thm -> thm
     1.8    val guess_instance: thm -> int -> thm -> thm Seq.seq
     1.9    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    1.10      thm list -> int -> cases_tactic
    1.11 @@ -205,11 +206,6 @@
    1.12  fun rule_instance thy inst rule =
    1.13    Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
    1.14  
    1.15 -fun mutual_rule ths =
    1.16 -  (case RuleCases.mutual_rule ths of
    1.17 -    NONE => error "Failed to join given rules into one mutual rule"
    1.18 -  | SOME res => res);
    1.19 -
    1.20  fun internalize k th =
    1.21    th |> Thm.permute_prems 0 k
    1.22    |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm);
    1.23 @@ -394,7 +390,7 @@
    1.24  
    1.25      val ruleq =
    1.26        (case opt_rule of
    1.27 -        SOME rs => Seq.single (inst_rule (mutual_rule rs))
    1.28 +        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule rs))
    1.29        | NONE =>
    1.30            (find_inductS ctxt facts @
    1.31              map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))