diff -r 36e2fae2c68a -r ecdfc96cf4d0 src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Fri Aug 04 12:01:31 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Fri Aug 04 18:01:45 2006 +0200
@@ -103,14 +103,13 @@
 end
 
 
-
 fun split_some_equations ctx eqns =
     let
-      fun split_aux prevs [] = []
+      fun split_aux prev [] = []
         | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
                                                           :: split_aux (eq :: prev) es
         | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) 
-                                                                :: split_aux (eq :: prev) es
+                                                           :: split_aux (eq :: prev) es
     in
       split_aux [] eqns
     end