src/Pure/Tools/compute.ML

--- a/src/Pure/Tools/compute.ML	Thu Sep 01 18:48:54 2005 +0200
+++ b/src/Pure/Tools/compute.ML	Thu Sep 01 22:15:10 2005 +0200
@@ -44,13 +44,13 @@
 val remove_types =
     let
         fun remove_types_var table invtable ccount vcount ldepth t =
-            (case Termtab.lookup (table, t) of
+            (case Termtab.curried_lookup table t of
                  NONE =>
                  let
                      val a = AbstractMachine.Var vcount
                  in
-                     (Termtab.update ((t, a), table),
-                      AMTermTab.update ((a, t), invtable),
+                     (Termtab.curried_update (t, a) table,
+                      AMTermTab.curried_update (a, t) invtable,
                       ccount,
                       inc vcount,
                       AbstractMachine.Var (add vcount ldepth))
@@ -60,13 +60,13 @@
                | SOME _ => sys_error "remove_types_var: lookup should be a var")
 
         fun remove_types_const table invtable ccount vcount ldepth t =
-            (case Termtab.lookup (table, t) of
+            (case Termtab.curried_lookup table t of
                  NONE =>
                  let
                      val a = AbstractMachine.Const ccount
                  in
-                     (Termtab.update ((t, a), table),
-                      AMTermTab.update ((a, t), invtable),
+                     (Termtab.curried_update (t, a) table,
+                      AMTermTab.curried_update (a, t) invtable,
                       inc ccount,
                       vcount,
                       a)
@@ -114,12 +114,12 @@
     let
         fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
             if v < ldepth then (Bound v, List.nth (bounds, v)) else
-            (case AMTermTab.lookup (invtable, AbstractMachine.Var (v-ldepth)) of
+            (case AMTermTab.curried_lookup invtable (AbstractMachine.Var (v-ldepth)) of
                  SOME (t as Var (_, ty)) => (t, ty)
                | SOME (t as Free (_, ty)) => (t, ty)
                | _ => sys_error "infer_types: lookup should deliver Var or Free")
           | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
-            (case AMTermTab.lookup (invtable, c) of
+            (case AMTermTab.curried_lookup invtable c of
                  SOME (c as Const (_, ty)) => (c, ty)
                | _ => sys_error "infer_types: lookup should deliver Const")
           | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
@@ -176,10 +176,10 @@
 
                 fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
                     let
-                        val var' = valOf (AMTermTab.lookup (invtable, var))
+                        val var' = valOf (AMTermTab.curried_lookup invtable var)
                         val table = Termtab.delete var' table
                         val invtable = AMTermTab.delete var invtable
-                        val vars = Inttab.update_new ((v, n), vars) handle Inttab.DUP _ =>
+                        val vars = Inttab.curried_update_new (v, n) vars handle Inttab.DUP _ =>
                           raise (Make "no duplicate variable in pattern allowed")
                     in
                         (table, invtable, n+1, vars, AbstractMachine.PVar)
@@ -217,7 +217,7 @@
 
                 fun rename ldepth vars (var as AbstractMachine.Var v) =
                     if v < ldepth then var
-                    else (case Inttab.lookup (vars, v-ldepth) of
+                    else (case Inttab.curried_lookup vars (v - ldepth) of
                               NONE => raise (Make "new variable on right hand side")
                             | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
                   | rename ldepth vars (c as AbstractMachine.Const _) = c
@@ -231,14 +231,12 @@
             end
 
         val (table, invtable, ccount, rules) =
-            List.foldl (fn (th, (table, invtable, ccount, rules)) =>
-                           let
-                               val (table, invtable, ccount, rule) =
-                                   thm2rule table invtable ccount th
-                           in
-                               (table, invtable, ccount, rule::rules)
-                           end)
-                       (Termtab.empty, AMTermTab.empty, 0, []) (List.rev ths)
+          fold_rev (fn th => fn (table, invtable, ccount, rules) =>
+            let
+              val (table, invtable, ccount, rule) =
+                  thm2rule table invtable ccount th
+            in (table, invtable, ccount, rule::rules) end)
+          ths (Termtab.empty, AMTermTab.empty, 0, [])
 
         val prog = AbstractMachine.compile rules