guess_instance: proper context;
authorwenzelm
Sun May 18 15:04:17 2008 +0200 (2008-05-18)
changeset 2694080df961f7900
parent 26939 1035c89b4c02
child 26941 fe007ee497c1
guess_instance: proper context;
src/HOL/Nominal/nominal_induct.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sun May 18 15:04:09 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun May 18 15:04:17 2008 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4                  (nth_list fixings (j - 1))))
     1.5            THEN' Induct.inner_atomize_tac) j))
     1.6          THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
     1.7 -            Induct.guess_instance
     1.8 +            Induct.guess_instance ctxt
     1.9                (finish_rule (Induct.internalize more_consumes rule)) i st'
    1.10              |> Seq.maps (fn rule' =>
    1.11                CASES (rule_cases rule' cases)
     2.1 --- a/src/Tools/induct.ML	Sun May 18 15:04:09 2008 +0200
     2.2 +++ b/src/Tools/induct.ML	Sun May 18 15:04:17 2008 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4    val rulified_term: thm -> theory * term
     2.5    val rulify_tac: int -> tactic
     2.6    val internalize: int -> thm -> thm
     2.7 -  val guess_instance: thm -> int -> thm -> thm Seq.seq
     2.8 +  val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
     2.9    val cases_tac: Proof.context -> term option list list -> thm option ->
    2.10      thm list -> int -> cases_tactic
    2.11    val induct_tac: Proof.context -> (string option * term) option list list ->
    2.12 @@ -420,16 +420,16 @@
    2.13  
    2.14  in
    2.15  
    2.16 -fun guess_instance rule i st =
    2.17 +fun guess_instance ctxt rule i st =
    2.18    let
    2.19 -    val thy = Thm.theory_of_thm st;
    2.20 +    val thy = ProofContext.theory_of ctxt;
    2.21      val maxidx = Thm.maxidx_of st;
    2.22      val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
    2.23      val params = rev (rename_wrt_term goal (Logic.strip_params goal));
    2.24    in
    2.25      if not (null params) then
    2.26        (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
    2.27 -        commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
    2.28 +        commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params));
    2.29        Seq.single rule)
    2.30      else
    2.31        let
    2.32 @@ -605,7 +605,7 @@
    2.33                  (nth_list arbitrary (j - 1))))
    2.34            THEN' inner_atomize_tac) j))
    2.35          THEN' atomize_tac) i st |> Seq.maps (fn st' =>
    2.36 -            guess_instance (internalize more_consumes rule) i st'
    2.37 +            guess_instance ctxt (internalize more_consumes rule) i st'
    2.38              |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
    2.39              |> Seq.maps (fn rule' =>
    2.40                CASES (rule_cases rule' cases)
    2.41 @@ -661,7 +661,7 @@
    2.42        ruleq goal
    2.43        |> Seq.maps (RuleCases.consume [] facts)
    2.44        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    2.45 -        guess_instance rule i st
    2.46 +        guess_instance ctxt rule i st
    2.47          |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
    2.48          |> Seq.maps (fn rule' =>
    2.49            CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)