--- 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