# 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)};