# HG changeset patch
# User haftmann
# Date 1193132891 -7200
# Node ID 6155f2faf23e8f5875f0ff7f167459f0ebabbb87
# Parent  af3c7e99fed03a4faa7350a6ee55bea79844f21b
tuned

diff -r af3c7e99fed0 -r 6155f2faf23e 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;