# HG changeset patch
# User haftmann
# Date 1236783410 -3600
# Node ID 4caf15ae8c2652b62be1ed610bdb9ed1220506ea
# Parent  0c7e1578036c427aeddadbe2fd8253ddc465146e
tuned

diff -r 0c7e1578036c -r 4caf15ae8c26 src/HOL/Tools/function_package/fundef_lib.ML
--- 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