--- a/src/Pure/envir.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/envir.ML Mon Jan 29 14:16:13 1996 +0100
@@ -18,19 +18,19 @@
datatype env = Envir of {asol: term xolist,
iTs: (indexname * typ) list,
maxidx: int}
- val alist_of : env -> (indexname * term) list
- val alist_of_olist : 'a xolist -> (indexname * 'a) list
- val empty : int->env
- val is_empty : env -> bool
- val minidx : env -> int option
- val genvar : string -> env * typ -> env * term
- val genvars : string -> env * typ list -> env * term list
- val lookup : env * indexname -> term option
- val norm_term : env -> term -> term
- val null_olist : 'a xolist
- val olist_of_alist : (indexname * 'a) list -> 'a xolist
- val update : (indexname * term) * env -> env
- val vupdate : (indexname * term) * env -> env
+ val alist_of : env -> (indexname * term) list
+ val alist_of_olist : 'a xolist -> (indexname * 'a) list
+ val empty : int->env
+ val is_empty : env -> bool
+ val minidx : env -> int option
+ val genvar : string -> env * typ -> env * term
+ val genvars : string -> env * typ list -> env * term list
+ val lookup : env * indexname -> term option
+ val norm_term : env -> term -> term
+ val null_olist : 'a xolist
+ val olist_of_alist : (indexname * 'a) list -> 'a xolist
+ val update : (indexname * term) * env -> env
+ val vupdate : (indexname * term) * env -> env
end;
functor EnvirFun () : ENVIR =