src/Pure/tactic.ML
changeset 15671 8df681866dc9
parent 15574 b1d1b5bfc464
child 15696 1da4ce092c0b
     1.1 --- a/src/Pure/tactic.ML	Thu Apr 07 09:27:33 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Apr 07 09:27:50 2005 +0200
     1.3 @@ -229,8 +229,7 @@
     1.4  	    and rts = types_sorts rule and (types,sorts) = types_sorts st
     1.5  	    fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm)
     1.6  	      | types'(ixn) = types ixn;
     1.7 -	    val used = add_term_tvarnames
     1.8 -	                  (prop_of st $ prop_of rule,[])
     1.9 +	    val used = Drule.add_used rule (Drule.add_used st []);
    1.10  	in read_insts sign rts (types',sorts) used sinsts end;
    1.11  
    1.12  (*Lift and instantiate a rule wrt the given state and subgoal number *)