--- a/src/HOL/Tools/function_package/fundef_lib.ML Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Wed Mar 11 15:56:50 2009 +0100
@@ -167,12 +167,10 @@
end
(* instance for unions *)
-fun regroup_union_conv t =
- regroup_conv (@{const_name Set.empty})
- @{const_name Un}
- (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
- @{thms "Un_empty_right"} @
- @{thms "Un_empty_left"})) t
+fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un}
+ (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
+ @{thms "Un_empty_right"} @
+ @{thms "Un_empty_left"})) t
end