src/Pure/tactic.ML
changeset 4178 e64ff1c1bc70
parent 3991 4cb2f2422695
child 4213 cef5ef41e70d
     1.1 --- a/src/Pure/tactic.ML	Wed Nov 05 19:40:50 1997 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Nov 06 10:28:20 1997 +0100
     1.3 @@ -351,7 +351,14 @@
     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 = res_inst_tac [("psi", sprop)] cut_rl;
     1.8 +fun subgoal_tac sprop i st = 
     1.9 +  let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
    1.10 +      val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
    1.11 +  in  
    1.12 +      if null (term_tvars concl') then ()
    1.13 +      else warning"Type variables in new subgoal: add a type constraint?";
    1.14 +      Sequence.single st'
    1.15 +  end;
    1.16  
    1.17  (*Introduce a list of lemmas and subgoals*)
    1.18  fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);