src/Pure/context.ML

--- a/src/Pure/context.ML	Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/context.ML	Thu Sep 01 18:48:50 2005 +0200
@@ -121,7 +121,7 @@
 val kinds = ref (Inttab.empty: kind Inttab.table);
 
 fun invoke meth_name meth_fn k =
-  (case Inttab.lookup (! kinds, k) of
+  (case Inttab.curried_lookup (! kinds) k of
     SOME kind => meth_fn kind |> transform_failure (fn exn =>
       DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
@@ -140,7 +140,7 @@
     val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
     val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
       warning ("Duplicate declaration of theory data " ^ quote name));
-    val _ = kinds := Inttab.update ((k, kind), ! kinds);
+    val _ = change kinds (Inttab.curried_update (k, kind));
   in k end;
 
 val copy_data = Inttab.map' invoke_copy;
@@ -256,7 +256,7 @@
   if draft_id id orelse Inttab.defined ids (#1 id) then ids
   else if Inttab.exists (equal (#2 id) o #2) ids then
     raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
-  else Inttab.update (id, ids);
+  else Inttab.curried_update id ids;
 
 fun check_insert intermediate id (ids, iids) =
   let val ids' = check_ins id ids and iids' = check_ins id iids
@@ -423,12 +423,12 @@
 val declare = declare_theory_data;
 
 fun get k dest thy =
-  (case Inttab.lookup (#theory (data_of thy), k) of
+  (case Inttab.curried_lookup (#theory (data_of thy)) k of
     SOME x => (dest x handle Match =>
       error ("Failed to access theory data " ^ quote (invoke_name k)))
   | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
 
-fun put k mk x = modify_thy (map_theory (curry Inttab.update (k, mk x)));
+fun put k mk x = modify_thy (map_theory (Inttab.curried_update (k, mk x)));
 fun init k = put k I (invoke_empty k);
 
 end;
@@ -525,7 +525,7 @@
 val kinds = ref (Inttab.empty: kind Inttab.table);
 
 fun invoke meth_name meth_fn k =
-  (case Inttab.lookup (! kinds, k) of
+  (case Inttab.curried_lookup (! kinds) k of
     SOME kind => meth_fn kind |> transform_failure (fn exn =>
       DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
@@ -549,18 +549,18 @@
     val kind = {name = name, init = init};
     val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
       warning ("Duplicate declaration of proof data " ^ quote name));
-    val _ = kinds := Inttab.update ((k, kind), ! kinds);
+    val _ = change kinds (Inttab.curried_update (k, kind));
   in k end;
 
-fun init k = modify_thy (map_proof (curry Inttab.update (k, ())));
+fun init k = modify_thy (map_proof (Inttab.curried_update (k, ())));
 
 fun get k dest prf =
-  (case Inttab.lookup (data_of_proof prf, k) of
+  (case Inttab.curried_lookup (data_of_proof prf) k of
     SOME x => (dest x handle Match =>
       error ("Failed to access proof data " ^ quote (invoke_name k)))
   | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
 
-fun put k mk x = map_prf (curry Inttab.update (k, mk x));
+fun put k mk x = map_prf (Inttab.curried_update (k, mk x));
 
 end;