# HG changeset patch
# User wenzelm
# Date 1011908534 -3600
# Node ID afa356dbcb15e12d643fdac0f2706655845d2c9f
# Parent  0fce95478e1985377cc34e86fb3bd1ac941b9702
fixed subgoal_tac; fails on non-existent subgoal;

diff -r 0fce95478e19 -r afa356dbcb15 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Jan 24 22:41:44 2002 +0100
+++ b/src/Pure/tactic.ML	Thu Jan 24 22:42:14 2002 +0100
@@ -351,14 +351,13 @@
     EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
 
 (*Introduce the given proposition as a lemma and subgoal*)
-fun subgoal_tac sprop i st =
-  let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
-      val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
-  in
+fun subgoal_tac sprop =
+  DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
+    let val concl' = Logic.strip_assums_concl prop in
       if null (term_tvars concl') then ()
       else warning"Type variables in new subgoal: add a type constraint?";
-      Seq.single st'
-  end;
+      all_tac
+  end);
 
 (*Introduce a list of lemmas and subgoals*)
 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);