tuned
authorhaftmann
Tue, 23 Oct 2007 11:48:11 +0200
changeset 25154 6155f2faf23e
parent 25153 af3c7e99fed0
child 25155 65612c9f7381
tuned
src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Oct 23 11:48:10 2007 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Oct 23 11:48:11 2007 +0200
@@ -45,8 +45,8 @@
   let
     fun index (x :: xs) tab =
       (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))
+        NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
+      | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
     | index [] _ = [];
   in index names [] end;