src/HOL/Nominal/nominal_induct.ML
changeset 33368 b1cf34f1855c
parent 32952 aeb1e44fbc19
child 33955 fff6f11b1f09
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  sig
     1.5    val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     1.6      (string * typ) list -> (string * typ) list list -> thm list ->
     1.7 -    thm list -> int -> RuleCases.cases_tactic
     1.8 +    thm list -> int -> Rule_Cases.cases_tactic
     1.9    val nominal_induct_method: (Proof.context -> Proof.method) context_parser
    1.10  end =
    1.11  struct
    1.12 @@ -31,9 +31,9 @@
    1.13  
    1.14  fun inst_mutual_rule ctxt insts avoiding rules =
    1.15    let
    1.16 -    val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
    1.17 +    val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules;
    1.18      val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
    1.19 -    val (cases, consumes) = RuleCases.get joined_rule;
    1.20 +    val (cases, consumes) = Rule_Cases.get joined_rule;
    1.21  
    1.22      val l = length rules;
    1.23      val _ =
    1.24 @@ -93,12 +93,12 @@
    1.25        split_all_tuples
    1.26        #> rename_params_rule true
    1.27          (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    1.28 -    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    1.29 +    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    1.30    in
    1.31      (fn i => fn st =>
    1.32        rules
    1.33        |> inst_mutual_rule ctxt insts avoiding
    1.34 -      |> RuleCases.consume (flat defs) facts
    1.35 +      |> Rule_Cases.consume (flat defs) facts
    1.36        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.37          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.38            (CONJUNCTS (ALLGOALS