diff src/elab_env.sml @ 5:258261a53842

Elaborating files
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 16:02:47 -0500
parents 64f09f7822c3
children 14b533dbe6cc
line wrap: on
line diff
--- a/src/elab_env.sml	Sat Jan 26 15:29:09 2008 -0500
+++ b/src/elab_env.sml	Sat Jan 26 16:02:47 2008 -0500
@@ -75,15 +75,17 @@
     (List.nth (#relC env, n))
     handle Subscript => raise UnboundRel n
 
-fun pushCNamed (env : env) x k =
+fun pushCNamedAs (env : env) x n k =
+    {renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
+     relC = #relC env,
+     namedC = IM.insert (#namedC env, n, (x, k))}
+
+fun pushCNamed env x k =
     let
         val n = !namedCounter
     in
         namedCounter := n + 1;
-        ({renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
-          relC = #relC env,
-          namedC = IM.insert (#namedC env, n, (x, k))},
-         n)
+        (pushCNamedAs env x n k, n)
     end
 
 fun lookupCNamed (env : env) n =