# HG changeset patch
# User wenzelm
# Date 1322833045 -3600
# Node ID b545ea8bc731843bd470e430ad3c79858feadfd1
# Parent  0430f9123e439aa2938a0b6feaf1593865db614d
tuned whitespace;

diff -r 0430f9123e43 -r b545ea8bc731 src/HOL/Tools/Datatype/datatype_prop.ML
--- 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 =