src/Pure/subgoal.ML
changeset 32210 a5e9d9f3e5e1
parent 32200 2bd8ab91a426
child 32213 f1b166317ae2
     1.1 --- a/src/Pure/subgoal.ML	Sun Jul 26 18:58:02 2009 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Sun Jul 26 19:38:02 2009 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
     1.5      asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
     1.6    val focus: Proof.context -> int -> thm -> focus * thm
     1.7 -  val retrofit: Proof.context -> (string * cterm) list -> cterm list ->
     1.8 +  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
     1.9      int -> thm -> thm -> thm Seq.seq
    1.10    val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.11    val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
    1.12 @@ -79,18 +79,20 @@
    1.13      val th' = fold (Thm.elim_implies o unlift) subgoals th;
    1.14    in (subgoals, th') end;
    1.15  
    1.16 -fun retrofit ctxt params asms i th =
    1.17 +fun retrofit ctxt1 ctxt0 params asms i state1 state0 =
    1.18    let
    1.19      val ps = map #2 params;
    1.20 -    val res0 = Goal.conclude th;
    1.21 -    val (res1, ctxt1) = lift_import ps res0 ctxt;
    1.22 +    val res = Goal.conclude state1;
    1.23 +    val (res1, ctxt2) = lift_import ps res ctxt1;
    1.24      val (subgoals, res2) = lift_subgoals params asms res1;
    1.25      val result = res2
    1.26        |> Drule.implies_intr_list asms
    1.27        |> Drule.forall_intr_list ps
    1.28        |> Drule.implies_intr_list subgoals
    1.29 -      |> singleton (Variable.export ctxt1 ctxt);
    1.30 -  in Thm.compose_no_flatten false (result, Thm.nprems_of res0) i end;
    1.31 +      |> singleton (Variable.export ctxt2 ctxt0)
    1.32 +      |> Drule.zero_var_indexes
    1.33 +      |> Drule.incr_indexes state0;
    1.34 +  in Thm.compose_no_flatten false (result, Thm.nprems_of state1) i state0 end;
    1.35  
    1.36  
    1.37  (* tacticals *)
    1.38 @@ -99,7 +101,7 @@
    1.39    if Thm.nprems_of st < i then Seq.empty
    1.40    else
    1.41      let val (args as {context, params, asms, ...}, st') = focus ctxt i st;
    1.42 -    in Seq.lifts (retrofit context params asms i) (tac args st') st end;
    1.43 +    in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
    1.44  
    1.45  fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
    1.46