# HG changeset patch
# User haftmann
# Date 1316212827 -7200
# Node ID 64469ea4373580d1ed1ae2a7382d89df8144ae68
# Parent  2625de88c994b2544e047b54cdeb57cdc5a0aabc
tuned spacing

diff -r 2625de88c994 -r 64469ea43735 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Sep 17 00:37:21 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Sat Sep 17 00:40:27 2011 +0200
@@ -79,8 +79,8 @@
   val empty = {splits = [], inj_consts = [], discrete = []};
   val extend = I;
   fun merge
-   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
-    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
+   ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1},
+    {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T =
    {splits = Thm.merge_thms (splits1, splits2),
     inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
     discrete = Library.merge (op =) (discrete1, discrete2)};