src/Pure/sign.ML
changeset 1576 af8f43f742a0
parent 1501 bb7f99a0a6f0
child 1580 e3fd931e6095
     1.1 --- a/src/Pure/sign.ML	Wed Mar 13 11:56:15 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Mar 14 10:40:21 1996 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4        Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
     1.5      | TFree _ => tvars
     1.6      | TVar(v as (a,S)) =>
     1.7 -        (case assoc(tvars,a) of
     1.8 +        (case assoc_string_int(tvars,a) of
     1.9             Some(S') => if S=S' then tvars
    1.10                         else raise_type
    1.11                              ("Type variable "^Syntax.string_of_vname a^
    1.12 @@ -238,7 +238,7 @@
    1.13            Const(c,T) => (vars, nodup_TVars(tvars,T))
    1.14          | Free(a,T) => (vars, nodup_TVars(tvars,T))
    1.15          | Var(v as (ixn,T)) =>
    1.16 -            (case assoc(vars,ixn) of
    1.17 +            (case assoc_string_int(vars,ixn) of
    1.18                 Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
    1.19                             else raise_type
    1.20                               ("Variable "^Syntax.string_of_vname ixn^