src/Pure/tactic.ML
changeset 8129 29e239c7b8c2
parent 7596 c97c3ad15d2e
child 8977 dd8bc754a072
     1.1 --- a/src/Pure/tactic.ML	Fri Jan 14 12:17:53 2000 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Jan 17 14:10:32 2000 +0100
     1.3 @@ -222,8 +222,8 @@
     1.4      val used = add_term_tvarnames
     1.5                    (#prop(rep_thm st) $ #prop(rep_thm rule),[])
     1.6      val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
     1.7 -in instantiate (map lifttvar Tinsts, map liftpair insts)
     1.8 -               (lift_rule (st,i) rule)
     1.9 +in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    1.10 +                     (lift_rule (st,i) rule)
    1.11  end;
    1.12  
    1.13  (*
    1.14 @@ -251,8 +251,8 @@
    1.15      (*lift only Var, not term, which must be lifted already*)
    1.16      fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
    1.17      fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
    1.18 -in instantiate (map liftTpair Tinsts, map liftpair insts)
    1.19 -               (lift_rule (st,i) rule)
    1.20 +in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.21 +                     (lift_rule (st,i) rule)
    1.22  end;
    1.23  
    1.24  (*** Resolve after lifting and instantation; may refer to parameters of the