src/Pure/type.ML
changeset 17412 e26cb20ef0cc
parent 17221 6cd180204582
child 17496 26535df536ae
     1.1 --- a/src/Pure/type.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4              val Ts' = map cert Ts;
     1.5              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
     1.6            in
     1.7 -            (case Symtab.curried_lookup types c of
     1.8 +            (case Symtab.lookup types c of
     1.9                SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
    1.10              | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
    1.11                  if syn then check_syntax c else ();
    1.12 @@ -284,7 +284,7 @@
    1.13    [TVar (ixn, S), TVar (ixn, S')], []);
    1.14  
    1.15  fun lookup (tye, (ixn, S)) =
    1.16 -  (case Vartab.curried_lookup tye ixn of
    1.17 +  (case Vartab.lookup tye ixn of
    1.18      NONE => NONE
    1.19    | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
    1.20  
    1.21 @@ -298,7 +298,7 @@
    1.22      fun match (TVar (v, S), T) subs =
    1.23            (case lookup (subs, (v, S)) of
    1.24              NONE =>
    1.25 -              if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs
    1.26 +              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
    1.27                else raise TYPE_MATCH
    1.28            | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.29        | match (Type (a, Ts), Type (b, Us)) subs =
    1.30 @@ -317,7 +317,7 @@
    1.31  (*purely structural matching*)
    1.32  fun raw_match (TVar (v, S), T) subs =
    1.33        (case lookup (subs, (v, S)) of
    1.34 -        NONE => Vartab.curried_update_new (v, (S, T)) subs
    1.35 +        NONE => Vartab.update_new (v, (S, T)) subs
    1.36        | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.37    | raw_match (Type (a, Ts), Type (b, Us)) subs =
    1.38        if a <> b then raise TYPE_MATCH
    1.39 @@ -366,7 +366,7 @@
    1.40      fun meet (_, []) tye = tye
    1.41        | meet (TVar (xi, S'), S) tye =
    1.42            if Sorts.sort_le classes (S', S) then tye
    1.43 -          else Vartab.curried_update_new
    1.44 +          else Vartab.update_new
    1.45              (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye
    1.46        | meet (TFree (_, S'), S) tye =
    1.47            if Sorts.sort_le classes (S', S) then tye
    1.48 @@ -381,19 +381,19 @@
    1.49            if eq_ix (v, w) then
    1.50              if S1 = S2 then tye else tvar_clash v S1 S2
    1.51            else if Sorts.sort_le classes (S1, S2) then
    1.52 -            Vartab.curried_update_new (w, (S2, T)) tye
    1.53 +            Vartab.update_new (w, (S2, T)) tye
    1.54            else if Sorts.sort_le classes (S2, S1) then
    1.55 -            Vartab.curried_update_new (v, (S1, U)) tye
    1.56 +            Vartab.update_new (v, (S1, U)) tye
    1.57            else
    1.58              let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
    1.59 -              Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye)
    1.60 +              Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye)
    1.61              end
    1.62        | (TVar (v, S), T) =>
    1.63            if occurs v tye T then raise TUNIFY
    1.64 -          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
    1.65 +          else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
    1.66        | (T, TVar (v, S)) =>
    1.67            if occurs v tye T then raise TUNIFY
    1.68 -          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
    1.69 +          else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
    1.70        | (Type (a, Ts), Type (b, Us)) =>
    1.71            if a <> b then raise TUNIFY
    1.72            else unifs (Ts, Us) tye
    1.73 @@ -408,13 +408,13 @@
    1.74      (T as TVar (v, S1), U as TVar (w, S2)) =>
    1.75        if eq_ix (v, w) then
    1.76          if S1 = S2 then tye else tvar_clash v S1 S2
    1.77 -      else Vartab.curried_update_new (w, (S2, T)) tye
    1.78 +      else Vartab.update_new (w, (S2, T)) tye
    1.79    | (TVar (v, S), T) =>
    1.80        if occurs v tye T then raise TUNIFY
    1.81 -      else Vartab.curried_update_new (v, (S, T)) tye
    1.82 +      else Vartab.update_new (v, (S, T)) tye
    1.83    | (T, TVar (v, S)) =>
    1.84        if occurs v tye T then raise TUNIFY
    1.85 -      else Vartab.curried_update_new (v, (S, T)) tye
    1.86 +      else Vartab.update_new (v, (S, T)) tye
    1.87    | (Type (a, Ts), Type (b, Us)) =>
    1.88        if a <> b then raise TUNIFY
    1.89        else raw_unifys (Ts, Us) tye
    1.90 @@ -476,9 +476,9 @@
    1.91  
    1.92  fun insert_arities pp classes (t, ars) arities =
    1.93    let val ars' =
    1.94 -    Symtab.curried_lookup_multi arities t
    1.95 +    Symtab.lookup_multi arities t
    1.96      |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
    1.97 -  in Symtab.curried_update (t, ars') arities end;
    1.98 +  in Symtab.update (t, ars') arities end;
    1.99  
   1.100  fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
   1.101    insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
   1.102 @@ -488,7 +488,7 @@
   1.103  fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   1.104    let
   1.105      fun prep (t, Ss, S) =
   1.106 -      (case Symtab.curried_lookup (#2 types) t of
   1.107 +      (case Symtab.lookup (#2 types) t of
   1.108          SOME (LogicalType n, _) =>
   1.109            if length Ss = n then
   1.110              (t, map (cert_sort tsig) Ss, cert_sort tsig S)
   1.111 @@ -591,18 +591,18 @@
   1.112      val c' = NameSpace.full naming c;
   1.113      val space' = NameSpace.declare naming c' space;
   1.114      val types' =
   1.115 -      (case Symtab.curried_lookup types c' of
   1.116 +      (case Symtab.lookup types c' of
   1.117          SOME (decl', _) => err_in_decls c' decl decl'
   1.118 -      | NONE => Symtab.curried_update (c', (decl, stamp ())) types);
   1.119 +      | NONE => Symtab.update (c', (decl, stamp ())) types);
   1.120    in (space', types') end;
   1.121  
   1.122 -fun the_decl (_, types) = fst o the o Symtab.curried_lookup types;
   1.123 +fun the_decl (_, types) = fst o the o Symtab.lookup types;
   1.124  
   1.125  fun change_types f = map_tsig (fn (classes, default, types, arities) =>
   1.126    (classes, default, f types, arities));
   1.127  
   1.128  fun syntactic types (Type (c, Ts)) =
   1.129 -      (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false)
   1.130 +      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
   1.131          orelse exists (syntactic types) Ts
   1.132    | syntactic _ _ = false;
   1.133