src/Pure/envir.ML
changeset 1460 5a6f2aabd538
parent 1458 fd510875fb71
child 1500 b2de3b3277b8
     1.1 --- a/src/Pure/envir.ML	Mon Jan 29 13:58:15 1996 +0100
     1.2 +++ b/src/Pure/envir.ML	Mon Jan 29 14:16:13 1996 +0100
     1.3 @@ -18,19 +18,19 @@
     1.4    datatype env = Envir of {asol: term xolist,
     1.5                             iTs: (indexname * typ) list,
     1.6                             maxidx: int}
     1.7 -  val alist_of          : env -> (indexname * term) list
     1.8 -  val alist_of_olist    : 'a xolist -> (indexname * 'a) list
     1.9 -  val empty             : int->env
    1.10 -  val is_empty          : env -> bool
    1.11 -  val minidx            : env -> int option
    1.12 -  val genvar            : string -> env * typ -> env * term
    1.13 -  val genvars           : string -> env * typ list -> env * term list
    1.14 -  val lookup            : env * indexname -> term option
    1.15 -  val norm_term         : env -> term -> term
    1.16 -  val null_olist        : 'a xolist
    1.17 -  val olist_of_alist    : (indexname * 'a) list -> 'a xolist
    1.18 -  val update            : (indexname * term) * env -> env
    1.19 -  val vupdate           : (indexname * term) * env -> env
    1.20 +  val alist_of		: env -> (indexname * term) list
    1.21 +  val alist_of_olist	: 'a xolist -> (indexname * 'a) list
    1.22 +  val empty		: int->env
    1.23 +  val is_empty		: env -> bool
    1.24 +  val minidx		: env -> int option
    1.25 +  val genvar		: string -> env * typ -> env * term
    1.26 +  val genvars		: string -> env * typ list -> env * term list
    1.27 +  val lookup		: env * indexname -> term option
    1.28 +  val norm_term		: env -> term -> term
    1.29 +  val null_olist	: 'a xolist
    1.30 +  val olist_of_alist	: (indexname * 'a) list -> 'a xolist
    1.31 +  val update		: (indexname * term) * env -> env
    1.32 +  val vupdate		: (indexname * term) * env -> env
    1.33  end;
    1.34  
    1.35  functor EnvirFun () : ENVIR =