# HG changeset patch
# User haftmann
# Date 1433177960 -7200
# Node ID 26700f36d6f1a758cdaad07cf9ff44cfa200be4c
# Parent  e66830e878e37557f1351ee6970f16914eaed6a1
tuned, including proper signature for functor argument

diff -r e66830e878e3 -r 26700f36d6f1 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -106,7 +106,7 @@
 val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false);
 
 
-structure LA_Data =
+structure LA_Data: LIN_ARITH_DATA =
 struct
 
 val neq_limit = neq_limit;
@@ -166,8 +166,7 @@
             (SOME s', SOME t') => SOME (mC $ s' $ t')
           | (SOME s', NONE) => SOME s'
           | (NONE, SOME t') =>
-               let val Const(_,T) = mC
-               in SOME (mC $ Const (@{const_name Groups.one}, domain_type T) $ t') end
+               SOME (mC $ Const (@{const_name Groups.one}, domain_type (snd (dest_Const mC))) $ t')
           | (NONE, NONE) => NONE,
           Rat.mult m' (Rat.inv p))
       end