# HG changeset patch
# User haftmann
# Date 1215533592 -7200
# Node ID 1505582668314a04dc083a1a971281aa49bf4a4b
# Parent  80d0de398339274c0161705f3f5502aa1f61cd24
clarified code

diff -r 80d0de398339 -r 150558266831 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Jul 08 18:13:11 2008 +0200
+++ b/src/Tools/nbe.ML	Tue Jul 08 18:13:12 2008 +0200
@@ -59,22 +59,22 @@
     Const of int * Univ list           (*named (uninterpreted) constants*)
   | Free of string * Univ list         (*free variables*)
   | DFree of string * int              (*free (uninterpreted) dictionary parameters*)
-  | BVar of int * Univ list            (*bound named variables*)
+  | BVar of int * Univ list            (*bound variables, named*)
   | Abs of (int * (Univ list -> Univ)) * Univ list
-                                      (*abstractions as closures*);
+                                       (*abstractions as closures*);
 
 (* constructor functions *)
 
 fun abss n f = Abs ((n, f), []);
 fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in
-      if k = 0 then f (ys @ xs)
-      else if k < 0 then
-        let val (zs, ws) = chop (~ k) ys
-        in apps (f (ws @ xs)) zs end
-      else Abs ((k, f), ys @ xs) end (*note: reverse convention also for apps!*)
+      case int_ord (k, 0)
+       of EQUAL => f (ys @ xs)
+        | LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end
+        | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*)
+      end
   | apps (Const (name, xs)) ys = Const (name, ys @ xs)
   | apps (Free (name, xs)) ys = Free (name, ys @ xs)
-  | apps (BVar (name, xs)) ys = BVar (name, ys @ xs);
+  | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
 
 
 (** assembling and compiling ML code from terms **)
@@ -332,8 +332,8 @@
           in of_apps bounds (Term.Const (c, T'), ts') typidx' end
       | of_univ bounds (Free (name, ts)) typidx =
           of_apps bounds (Term.Free (name, dummyT), ts) typidx
-      | of_univ bounds (BVar (name, ts)) typidx =
-          of_apps bounds (Bound (bounds - name - 1), ts) typidx
+      | of_univ bounds (BVar (n, ts)) typidx =
+          of_apps bounds (Bound (bounds - n - 1), ts) typidx
       | of_univ bounds (t as Abs _) typidx =
           typidx
           |> of_univ (bounds + 1) (apps t [BVar (bounds, [])])