Drule.add_used;
authorwenzelm
Thu Apr 07 09:27:50 2005 +0200 (2005-04-07)
changeset 156718df681866dc9
parent 15670 963cd3f7976c
child 15672 32aea1e31eb8
Drule.add_used;
src/Pure/tactic.ML
     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 *)