src/HOL/Tools/datatype_prop.ML
changeset 17521 0f1c48de39f5
parent 15574 b1d1b5bfc464
child 19233 77ca20b0ed77
--- a/src/HOL/Tools/datatype_prop.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -44,7 +44,7 @@
 fun indexify_names names =
   let
     fun index (x :: xs) tab =
-      (case assoc (tab, x) of
+      (case AList.lookup (op =) tab x of
         NONE => if x mem xs then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
       | SOME i => (x ^ Library.string_of_int i) :: index xs ((x, i + 1) :: tab))
     | index [] _ = [];