# HG changeset patch
# User wenzelm
# Date 1154550415 -7200
# Node ID 66b2a1f16bbbb6f2400d58c5bb9a03b8fc31e807
# Parent  963bf056e8f7ed2aecfdefae5a88bb15271ad316
Variable.focus_subgoal;

diff -r 963bf056e8f7 -r 66b2a1f16bbb src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Aug 02 22:26:54 2006 +0200
+++ b/src/Pure/subgoal.ML	Wed Aug 02 22:26:55 2006 +0200
@@ -30,7 +30,7 @@
 fun focus ctxt i st =
   let
     val ((schematics, [st']), ctxt') = Variable.import true [norm_hhf st] ctxt;
-    val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
+    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
     val asms = Drule.strip_imp_prems goal;
     val concl = Drule.strip_imp_concl goal;
     val (prems, context) = Assumption.add_assumes asms ctxt'';