src/Pure/envir.ML
changeset 19861 620d90091788
parent 19422 bba26da0f227
child 20098 19871ee094b1
     1.1 --- a/src/Pure/envir.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Pure/envir.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val update: ((indexname * typ) * term) * env -> env
     1.5    val empty: int -> env
     1.6    val is_empty: env -> bool
     1.7 -  val above: int * env -> bool
     1.8 +  val above: env -> int -> bool
     1.9    val vupdate: ((indexname * typ) * term) * env -> env
    1.10    val alist_of: env -> (indexname * (typ * term)) list
    1.11    val norm_term: env -> term -> term
    1.12 @@ -104,12 +104,9 @@
    1.13  fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
    1.14  
    1.15  (*Determine if the least index updated exceeds lim*)
    1.16 -fun above (lim, Envir {asol, iTs, ...}) =
    1.17 -  (case (Vartab.min_key asol, Vartab.min_key iTs) of
    1.18 -     (NONE, NONE) => true
    1.19 -   | (SOME (_, i), NONE) => i > lim
    1.20 -   | (NONE, SOME (_, i')) => i' > lim
    1.21 -   | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
    1.22 +fun above (Envir {asol, iTs, ...}) lim =
    1.23 +  (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
    1.24 +  (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
    1.25  
    1.26  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    1.27  fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of