--- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Dec 02 14:26:43 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Dec 02 14:37:25 2011 +0100
@@ -38,13 +38,13 @@
fun indexify_names names =
let
fun index (x :: xs) tab =
- (case AList.lookup (op =) tab x of
- 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 [] _ = [];
+ (case AList.lookup (op =) tab x of
+ 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;
fun make_tnames Ts =