1.1 --- a/src/HOL/Tools/lin_arith.ML	Thu May 29 23:46:36 2008 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu May 29 23:46:37 2008 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4       {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
     1.5        lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ->
     1.6      Context.generic -> Context.generic
     1.7 +  val warning_count: int ref
     1.8    val setup: Context.generic -> Context.generic
     1.9  end;
    1.10  
    1.11 @@ -780,14 +781,14 @@
    1.12  
    1.13  val lin_arith_pre_tac = LA_Data_Ref.pre_tac;
    1.14  
    1.15 -structure Fast_Arith =
    1.16 -  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
    1.17 +structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data_Ref);
    1.18  
    1.19  val map_data = Fast_Arith.map_data;
    1.20  
    1.21 -fun fast_arith_tac ctxt    = Fast_Arith.lin_arith_tac ctxt false;
    1.22 -val fast_ex_arith_tac      = Fast_Arith.lin_arith_tac;
    1.23 -val trace_arith            = Fast_Arith.trace;
    1.24 +fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    1.25 +val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
    1.26 +val trace_arith = Fast_Arith.trace;
    1.27 +val warning_count = Fast_Arith.warning_count;
    1.28  
    1.29  (* reduce contradictory <= to False.
    1.30     Most of the work is done by the cancel tactics. *)