src/Pure/tactic.ML
changeset 16876 f57b38cced32
parent 16809 8ca51a846576
child 16942 c01816b32c04
     1.1 --- a/src/Pure/tactic.ML	Tue Jul 19 17:21:46 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue Jul 19 17:21:47 2005 +0200
     1.3 @@ -256,13 +256,13 @@
     1.4      and params = params_of_state st i
     1.5      val paramTs = map #2 params
     1.6      and inc = maxidx+1
     1.7 -    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
     1.8 +    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
     1.9        | liftvar t = raise TERM("Variable expected", [t]);
    1.10      fun liftterm t = list_abs_free (params,
    1.11                                      Logic.incr_indexes(paramTs,inc) t)
    1.12      (*Lifts instantiation pair over params*)
    1.13      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    1.14 -    val lifttvar = pairself (ctyp_fun (incr_tvar inc))
    1.15 +    val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
    1.16  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    1.17                       (lift_rule (st,i) rule)
    1.18  end;
    1.19 @@ -289,12 +289,12 @@
    1.20  let val {maxidx,thy,...} = rep_thm st
    1.21      val paramTs = map #2 (params_of_state st i)
    1.22      and inc = maxidx+1
    1.23 -    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    1.24 +    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    1.25      (*lift only Var, not term, which must be lifted already*)
    1.26      fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
    1.27      fun liftTpair (((a, i), S), T) =
    1.28        (ctyp_of thy (TVar ((a, i + inc), S)),
    1.29 -       ctyp_of thy (incr_tvar inc T))
    1.30 +       ctyp_of thy (Logic.incr_tvar inc T))
    1.31  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.32                       (lift_rule (st,i) rule)
    1.33  end;