subgoal_tac displays a warning if the new subgoal has type variables
authorpaulson
Thu Nov 06 10:28:20 1997 +0100 (1997-11-06)
changeset 4178e64ff1c1bc70
parent 4177 77f65eb64da4
child 4179 cc4b6791d5dc
subgoal_tac displays a warning if the new subgoal has type variables
NEWS
src/Pure/tactic.ML
     1.1 --- a/NEWS	Wed Nov 05 19:40:50 1997 +0100
     1.2 +++ b/NEWS	Thu Nov 06 10:28:20 1997 +0100
     1.3 @@ -50,6 +50,8 @@
     1.4  
     1.5  * improved output of warnings (###) / errors (***);
     1.6  
     1.7 +* subgoal_tac displays a warning if the new subgoal has type variables;
     1.8 +
     1.9  * removed old README and Makefiles;
    1.10  
    1.11  * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
     2.1 --- a/src/Pure/tactic.ML	Wed Nov 05 19:40:50 1997 +0100
     2.2 +++ b/src/Pure/tactic.ML	Thu Nov 06 10:28:20 1997 +0100
     2.3 @@ -351,7 +351,14 @@
     2.4      EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
     2.5  
     2.6  (*Introduce the given proposition as a lemma and subgoal*)
     2.7 -fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl;
     2.8 +fun subgoal_tac sprop i st = 
     2.9 +  let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
    2.10 +      val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
    2.11 +  in  
    2.12 +      if null (term_tvars concl') then ()
    2.13 +      else warning"Type variables in new subgoal: add a type constraint?";
    2.14 +      Sequence.single st'
    2.15 +  end;
    2.16  
    2.17  (*Introduce a list of lemmas and subgoals*)
    2.18  fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);