src/Pure/context.ML
changeset 17412 e26cb20ef0cc
parent 17340 11f959f0fe6c
child 17756 d4a35f82fbb4
     1.1 --- a/src/Pure/context.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/Pure/context.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  val kinds = ref (Inttab.empty: kind Inttab.table);
     1.5  
     1.6  fun invoke meth_name meth_fn k =
     1.7 -  (case Inttab.curried_lookup (! kinds) k of
     1.8 +  (case Inttab.lookup (! kinds) k of
     1.9      SOME kind => meth_fn kind |> transform_failure (fn exn =>
    1.10        EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.11    | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
    1.12 @@ -137,7 +137,7 @@
    1.13      val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
    1.14      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    1.15        warning ("Duplicate declaration of theory data " ^ quote name));
    1.16 -    val _ = change kinds (Inttab.curried_update (k, kind));
    1.17 +    val _ = change kinds (Inttab.update (k, kind));
    1.18    in k end;
    1.19  
    1.20  val copy_data = Inttab.map' invoke_copy;
    1.21 @@ -253,7 +253,7 @@
    1.22    if draft_id id orelse Inttab.defined ids (#1 id) then ids
    1.23    else if Inttab.exists (equal (#2 id) o #2) ids then
    1.24      raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
    1.25 -  else Inttab.curried_update id ids;
    1.26 +  else Inttab.update id ids;
    1.27  
    1.28  fun check_insert intermediate id (ids, iids) =
    1.29    let val ids' = check_ins id ids and iids' = check_ins id iids
    1.30 @@ -420,12 +420,12 @@
    1.31  val declare = declare_theory_data;
    1.32  
    1.33  fun get k dest thy =
    1.34 -  (case Inttab.curried_lookup (#theory (data_of thy)) k of
    1.35 +  (case Inttab.lookup (#theory (data_of thy)) k of
    1.36      SOME x => (dest x handle Match =>
    1.37        error ("Failed to access theory data " ^ quote (invoke_name k)))
    1.38    | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
    1.39  
    1.40 -fun put k mk x = modify_thy (map_theory (Inttab.curried_update (k, mk x)));
    1.41 +fun put k mk x = modify_thy (map_theory (Inttab.update (k, mk x)));
    1.42  fun init k = put k I (invoke_empty k);
    1.43  
    1.44  end;
    1.45 @@ -522,7 +522,7 @@
    1.46  val kinds = ref (Inttab.empty: kind Inttab.table);
    1.47  
    1.48  fun invoke meth_name meth_fn k =
    1.49 -  (case Inttab.curried_lookup (! kinds) k of
    1.50 +  (case Inttab.lookup (! kinds) k of
    1.51      SOME kind => meth_fn kind |> transform_failure (fn exn =>
    1.52        EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
    1.53    | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
    1.54 @@ -546,18 +546,18 @@
    1.55      val kind = {name = name, init = init};
    1.56      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
    1.57        warning ("Duplicate declaration of proof data " ^ quote name));
    1.58 -    val _ = change kinds (Inttab.curried_update (k, kind));
    1.59 +    val _ = change kinds (Inttab.update (k, kind));
    1.60    in k end;
    1.61  
    1.62 -fun init k = modify_thy (map_proof (Inttab.curried_update (k, ())));
    1.63 +fun init k = modify_thy (map_proof (Inttab.update (k, ())));
    1.64  
    1.65  fun get k dest prf =
    1.66 -  (case Inttab.curried_lookup (data_of_proof prf) k of
    1.67 +  (case Inttab.lookup (data_of_proof prf) k of
    1.68      SOME x => (dest x handle Match =>
    1.69        error ("Failed to access proof data " ^ quote (invoke_name k)))
    1.70    | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
    1.71  
    1.72 -fun put k mk x = map_prf (Inttab.curried_update (k, mk x));
    1.73 +fun put k mk x = map_prf (Inttab.update (k, mk x));
    1.74  
    1.75  end;
    1.76