# HG changeset patch
# User wenzelm
# Date 1112858870 -7200
# Node ID 8df681866dc96009ff4e42de86ab9397129a53f3
# Parent  963cd3f7976c6a50f69bb03926c1edd1fce22b95
Drule.add_used;

diff -r 963cd3f7976c -r 8df681866dc9 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Apr 07 09:27:33 2005 +0200
+++ b/src/Pure/tactic.ML	Thu Apr 07 09:27:50 2005 +0200
@@ -229,8 +229,7 @@
 	    and rts = types_sorts rule and (types,sorts) = types_sorts st
 	    fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm)
 	      | types'(ixn) = types ixn;
-	    val used = add_term_tvarnames
-	                  (prop_of st $ prop_of rule,[])
+	    val used = Drule.add_used rule (Drule.add_used st []);
 	in read_insts sign rts (types',sorts) used sinsts end;
 
 (*Lift and instantiate a rule wrt the given state and subgoal number *)