1.1 --- a/src/Pure/tactic.ML	Thu Jan 24 22:41:44 2002 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Jan 24 22:42:14 2002 +0100
     1.3 @@ -351,14 +351,13 @@
     1.4      EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
     1.5  
     1.6  (*Introduce the given proposition as a lemma and subgoal*)
     1.7 -fun subgoal_tac sprop i st =
     1.8 -  let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
     1.9 -      val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
    1.10 -  in
    1.11 +fun subgoal_tac sprop =
    1.12 +  DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
    1.13 +    let val concl' = Logic.strip_assums_concl prop in
    1.14        if null (term_tvars concl') then ()
    1.15        else warning"Type variables in new subgoal: add a type constraint?";
    1.16 -      Seq.single st'
    1.17 -  end;
    1.18 +      all_tac
    1.19 +  end);
    1.20  
    1.21  (*Introduce a list of lemmas and subgoals*)
    1.22  fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);