RuleCases.mutual_rule: ctxt;
authorwenzelm
Sat Jun 17 19:37:43 2006 +0200 (2006-06-17)
changeset 19903158ea5884966
parent 19902 9e5d0df75c98
child 19904 9956ecabd9af
RuleCases.mutual_rule: ctxt;
Term.internal;
ProofContext.exports: simultaneous facts;
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Jun 17 18:58:12 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jun 17 19:37:43 2006 +0200
     1.3 @@ -30,10 +30,10 @@
     1.4  (* prepare rule *)
     1.5  
     1.6  (*conclusions: ?P avoiding_struct ... insts*)
     1.7 -fun inst_mutual_rule thy insts avoiding rules =
     1.8 +fun inst_mutual_rule ctxt insts avoiding rules =
     1.9    let
    1.10      val (concls, rule) =
    1.11 -      (case RuleCases.mutual_rule rules of
    1.12 +      (case RuleCases.mutual_rule ctxt rules of
    1.13          NONE => error "Failed to join given rules into one mutual rule"
    1.14        | SOME res => res);
    1.15      val (cases, consumes) = RuleCases.get rule;
    1.16 @@ -57,14 +57,14 @@
    1.17        end;
    1.18       val substs =
    1.19         map2 subst insts rules |> List.concat |> distinct (op =)
    1.20 -       |> map (pairself (Thm.cterm_of thy));
    1.21 +       |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
    1.22    in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
    1.23  
    1.24  fun rename_params_rule internal xs rule =
    1.25    let
    1.26      val tune =
    1.27 -      if internal then Syntax.internal
    1.28 -      else fn x => the_default x (try Syntax.dest_internal x);
    1.29 +      if internal then Term.internal
    1.30 +      else fn x => the_default x (try Term.dest_internal x);
    1.31      val n = length xs;
    1.32      fun rename prem =
    1.33        let
    1.34 @@ -97,7 +97,7 @@
    1.35    in
    1.36      (fn i => fn st =>
    1.37        rules
    1.38 -      |> inst_mutual_rule thy insts avoiding
    1.39 +      |> inst_mutual_rule ctxt insts avoiding
    1.40        |> RuleCases.consume (List.concat defs) facts
    1.41        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.42          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.43 @@ -113,7 +113,7 @@
    1.44              |> Seq.maps (fn rule' =>
    1.45                CASES (rule_cases rule' cases)
    1.46                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
    1.47 -                  PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
    1.48 +                  PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st'))))
    1.49      THEN_ALL_NEW_CASES InductMethod.rulify_tac
    1.50    end;
    1.51