src/HOL/Tools/lin_arith.ML
changeset 32863 5e8cef567042
parent 32740 9dd0a2f83429
child 33035 15eab423e573
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Oct 02 22:15:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Oct 02 23:15:36 2009 +0200
     1.3 @@ -767,8 +767,6 @@
     1.4  
     1.5  structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
     1.6  
     1.7 -val map_data = Fast_Arith.map_data;
     1.8 -
     1.9  fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    1.10    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
    1.11      lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};