src/Pure/tactic.ML
changeset 949 83c588d6fee9
parent 947 812ccc91bfa0
child 952 9e10962866b0
     1.1 --- a/src/Pure/tactic.ML	Sat Mar 11 17:46:14 1995 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Mar 13 09:38:10 1995 +0100
     1.3 @@ -197,9 +197,11 @@
     1.4      val rts = types_sorts rule and (types,sorts) = types_sorts state
     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 (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts
     1.8 +    val used = add_term_tvarnames
     1.9 +                  (#prop(rep_thm state) $ #prop(rep_thm rule),[])
    1.10 +    val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
    1.11  in instantiate (map lifttvar Tinsts, map liftpair insts)
    1.12 -		(lift_rule (state,i) rule)
    1.13 +               (lift_rule (state,i) rule)
    1.14  end;
    1.15  
    1.16