src/Pure/logic.ML
changeset 32023 2d071ac5032f
parent 32020 9abf5d66606e
child 32026 9898880061df
     1.1 --- a/src/Pure/logic.ML	Thu Jul 16 21:28:39 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jul 16 21:29:02 2009 +0200
     1.3 @@ -54,8 +54,9 @@
     1.4    val close_form: term -> term
     1.5    val combound: term * int * int -> term
     1.6    val rlist_abs: (string * typ) list * term -> term
     1.7 +  val incr_tvar_same: int -> typ Same.operation
     1.8 +  val incr_tvar: int -> typ -> typ
     1.9    val incr_indexes: typ list * int -> term -> term
    1.10 -  val incr_tvar: int -> typ -> typ
    1.11    val lift_abs: int -> term -> term -> term
    1.12    val lift_all: int -> term -> term -> term
    1.13    val strip_assums_hyp: term -> term list
    1.14 @@ -303,18 +304,20 @@
    1.15  fun rlist_abs ([], body) = body
    1.16    | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
    1.17  
    1.18 -
    1.19 -fun incrT k = Term_Subst.map_atypsT_same
    1.20 +fun incr_tvar_same k = Term_Subst.map_atypsT_same
    1.21    (fn TVar ((a, i), S) => TVar ((a, i + k), S)
    1.22      | _ => raise Same.SAME);
    1.23  
    1.24 +fun incr_tvar 0 T = T
    1.25 +  | incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
    1.26 +
    1.27  (*For all variables in the term, increment indexnames and lift over the Us
    1.28      result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
    1.29  fun incr_indexes ([], 0) t = t
    1.30    | incr_indexes (Ts, k) t =
    1.31        let
    1.32          val n = length Ts;
    1.33 -        val incrT = if k = 0 then I else incrT k;
    1.34 +        val incrT = if k = 0 then I else incr_tvar_same k;
    1.35  
    1.36          fun incr lev (Var ((x, i), T)) =
    1.37                combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
    1.38 @@ -329,9 +332,6 @@
    1.39            | incr _ (t as Bound _) = t;
    1.40        in incr 0 t handle Same.SAME => t end;
    1.41  
    1.42 -fun incr_tvar 0 T = T
    1.43 -  | incr_tvar k T = incrT k T handle Same.SAME => T;
    1.44 -
    1.45  
    1.46  (* Lifting functions from subgoal and increment:
    1.47      lift_abs operates on terms