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