--- a/src/HOL/Tools/datatype_prop.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Sun Feb 13 17:15:14 2005 +0100
@@ -45,8 +45,8 @@
let
fun index (x :: xs) tab =
(case assoc (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 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 [] _ = [];
in index names [] end;