# HG changeset patch
# User wenzelm
# Date 1249481850 -7200
# Node ID 4c21851036bf5fbc331f3f32f35b526beb203806
# Parent  f2fd9da84bacc24133f4e37b142a362f15a1cad8# Parent  1527ff8c2dfb8be0a8a68c46c72d45c9eddb6596
merged

diff -r f2fd9da84bac -r 4c21851036bf src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Tue Aug 04 23:25:00 2009 +0200
+++ b/src/Pure/subgoal.ML	Wed Aug 05 16:17:30 2009 +0200
@@ -102,7 +102,7 @@
 *)
 fun lift_subgoals params asms th =
   let
-    val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
+    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
     val unlift =
       fold (Thm.elim_implies o Thm.assume) asms o
       Drule.forall_elim_list (map #2 params) o Thm.assume;
@@ -133,14 +133,14 @@
 fun GEN_FOCUS flags tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
-    let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
-    in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
+    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
+    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
 
 val FOCUS_PARAMS = GEN_FOCUS (false, false);
 val FOCUS_PREMS = GEN_FOCUS (true, false);
 val FOCUS = GEN_FOCUS (true, true);
 
-fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
+fun SUBPROOF tac ctxt = FOCUS (Seq.map (tap (Goal.check_finished ctxt)) oo tac) ctxt;
 
 end;