Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/sign.ML
changeset 1576 af8f43f742a0
parent 1501 bb7f99a0a6f0
child 1580 e3fd931e6095 
--- a/src/Pure/sign.ML	Wed Mar 13 11:56:15 1996 +0100
+++ b/src/Pure/sign.ML	Thu Mar 14 10:40:21 1996 +0100
@@ -225,7 +225,7 @@
       Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
     | TFree _ => tvars
     | TVar(v as (a,S)) =>
-        (case assoc(tvars,a) of
+        (case assoc_string_int(tvars,a) of
            Some(S') => if S=S' then tvars
                        else raise_type
                             ("Type variable "^Syntax.string_of_vname a^
@@ -238,7 +238,7 @@
           Const(c,T) => (vars, nodup_TVars(tvars,T))
         | Free(a,T) => (vars, nodup_TVars(tvars,T))
         | Var(v as (ixn,T)) =>
-            (case assoc(vars,ixn) of
+            (case assoc_string_int(vars,ixn) of
                Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
                            else raise_type
                              ("Variable "^Syntax.string_of_vname ixn^
isabelle