# HG changeset patch
# User wenzelm
# Date 908893787 -7200
# Node ID ffecea5475013419da80339878fd488dc519b450
# Parent  7f582495967c428ecd9e0af2a9fbb9a549df871e
simple Env replaced by Symtab;

diff -r 7f582495967c -r ffecea547501 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Oct 20 16:29:08 1998 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue Oct 20 16:29:47 1998 +0200
@@ -165,16 +165,6 @@
 val stat_norm_ast = ref false;
 
 
-(* simple env *)
-
-structure Env =
-struct
-  val empty = [];
-  val add = op ::;
-  fun get (alist,x) = the (assoc (alist,x));
-end;
-
-
 (* match *)
 
 fun match ast pat =
@@ -185,7 +175,7 @@
           if a = b then env else raise NO_MATCH
       | mtch (Variable a) (Constant b) env =
           if a = b then env else raise NO_MATCH
-      | mtch ast (Variable x) env = Env.add ((x, ast), env)
+      | mtch ast (Variable x) env = Symtab.update ((x, ast), env)
       | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
       | mtch _ _ _ = raise NO_MATCH
     and mtch_lst (ast :: asts) (pat :: pats) env =
@@ -202,7 +192,7 @@
           end
       | _ => (ast, []));
   in
-    Some (mtch head pat Env.empty, args) handle NO_MATCH => None
+    Some (mtch head pat Symtab.empty, args) handle NO_MATCH => None
   end;
 
 
@@ -218,7 +208,7 @@
     val changes = ref 0;
 
     fun subst _ (ast as Constant _) = ast
-      | subst env (Variable x) = Env.get (env, x)
+      | subst env (Variable x) = the (Symtab.lookup (env, x))
       | subst env (Appl asts) = Appl (map (subst env) asts);
 
     fun try_rules ast ((lhs, rhs) :: pats) =