--- a/src/Pure/tactic.ML Sat Mar 11 17:46:14 1995 +0100
+++ b/src/Pure/tactic.ML Mon Mar 13 09:38:10 1995 +0100
@@ -197,9 +197,11 @@
val rts = types_sorts rule and (types,sorts) = types_sorts state
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
| types'(ixn) = types ixn;
- val (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts
+ val used = add_term_tvarnames
+ (#prop(rep_thm state) $ #prop(rep_thm rule),[])
+ val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
in instantiate (map lifttvar Tinsts, map liftpair insts)
- (lift_rule (state,i) rule)
+ (lift_rule (state,i) rule)
end;