# HG changeset patch
# User haftmann
# Date 1245051810 -7200
# Node ID e2272338dfcf67f2457c9109cf1a85259e404b23
# Parent  e1223f58ea9b80b7d75604b22de29ddedae103cf
made SML/NJ happy

diff -r e1223f58ea9b -r e2272338dfcf src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jun 15 08:16:09 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Jun 15 09:43:30 2009 +0200
@@ -122,7 +122,7 @@
 
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
                lessD = [], neqE = [], simpset = Simplifier.empty_ss,
-               number_of = (serial (), no_number_of) };
+               number_of = (serial (), no_number_of) } : T;
   val extend = I;
   fun merge _
     ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,