src/HOL/Tools/datatype_prop.ML
changeset 15531 08c8dad8e399
parent 15459 16dd63c78049
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_prop.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -45,8 +45,8 @@
     1.4    let
     1.5      fun index (x :: xs) tab =
     1.6        (case assoc (tab, x) of
     1.7 -        None => if x mem xs then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
     1.8 -      | Some i => (x ^ Library.string_of_int i) :: index xs ((x, i + 1) :: tab))
     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 [] _ = [];
    1.12    in index names [] end;
    1.13