1.1 --- a/src/Pure/subgoal.ML	Tue Aug 04 19:20:24 2009 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Wed Aug 05 15:39:34 2009 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  *)
     1.5  fun lift_subgoals params asms th =
     1.6    let
     1.7 -    val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
     1.8 +    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
     1.9      val unlift =
    1.10        fold (Thm.elim_implies o Thm.assume) asms o
    1.11        Drule.forall_elim_list (map #2 params) o Thm.assume;
    1.12 @@ -133,14 +133,14 @@
    1.13  fun GEN_FOCUS flags tac ctxt i st =
    1.14    if Thm.nprems_of st < i then Seq.empty
    1.15    else
    1.16 -    let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
    1.17 -    in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
    1.18 +    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
    1.19 +    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
    1.20  
    1.21  val FOCUS_PARAMS = GEN_FOCUS (false, false);
    1.22  val FOCUS_PREMS = GEN_FOCUS (true, false);
    1.23  val FOCUS = GEN_FOCUS (true, true);
    1.24  
    1.25 -fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
    1.26 +fun SUBPROOF tac ctxt = FOCUS (Seq.map (tap (Goal.check_finished ctxt)) oo tac) ctxt;
    1.27  
    1.28  end;
    1.29