# HG changeset patch
# User paulson
# Date 959260939 -7200
# Node ID dd8bc754a07277ab9aec6bb7c1737e661014bc70
# Parent  340d306f0118277781063d4ba951a9f88394ad61
res_inst_tac, etc., no longer print the "dest_state" message when the selected
subgoal does not exist

diff -r 340d306f0118 -r dd8bc754a072 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu May 25 15:20:44 2000 +0200
+++ b/src/Pure/tactic.ML	Thu May 25 15:22:19 2000 +0200
@@ -259,10 +259,12 @@
      subgoal.  Fails if "i" is out of range.  ***)
 
 (*compose version: arguments are as for bicompose.*)
-fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = st |>
-  (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
-   handle TERM (msg,_)   => (writeln msg;  no_tac)
-	| THM  (msg,_,_) => (writeln msg;  no_tac));
+fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = 
+  if i > nprems_of st then no_tac st
+  else st |>
+    (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
+     handle TERM (msg,_)   => (writeln msg;  no_tac)
+	  | THM  (msg,_,_) => (writeln msg;  no_tac));
 
 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   terms that are substituted contain (term or type) unknowns from the