# HG changeset patch
# User paulson
# Date 878808500 -3600
# Node ID e64ff1c1bc701858e49dbee91ed5984c9bcc0851
# Parent  77f65eb64da4dbd347cbad81603bad71c6bdf7e1
subgoal_tac displays a warning if the new subgoal has type variables

diff -r 77f65eb64da4 -r e64ff1c1bc70 NEWS
--- a/NEWS	Wed Nov 05 19:40:50 1997 +0100
+++ b/NEWS	Thu Nov 06 10:28:20 1997 +0100
@@ -50,6 +50,8 @@
 
 * improved output of warnings (###) / errors (***);
 
+* subgoal_tac displays a warning if the new subgoal has type variables;
+
 * removed old README and Makefiles;
 
 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
diff -r 77f65eb64da4 -r e64ff1c1bc70 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Nov 05 19:40:50 1997 +0100
+++ b/src/Pure/tactic.ML	Thu Nov 06 10:28:20 1997 +0100
@@ -351,7 +351,14 @@
     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 = res_inst_tac [("psi", sprop)] cut_rl;
+fun subgoal_tac sprop i st = 
+  let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
+      val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
+  in  
+      if null (term_tvars concl') then ()
+      else warning"Type variables in new subgoal: add a type constraint?";
+      Sequence.single st'
+  end;
 
 (*Introduce a list of lemmas and subgoals*)
 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);