# HG changeset patch
# User nipkow
# Date 1080920432 -7200
# Node ID 7ae3b247c6e90dd5775d712d111db4d450b4b236
# Parent  a183dec876ab3aa5f49de71f5bfa3b64bb0f9c4a
exposed fast_arith_neq_limit

diff -r a183dec876ab -r 7ae3b247c6e9 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Apr 02 17:37:45 2004 +0200
+++ b/src/HOL/arith_data.ML	Fri Apr 02 17:40:32 2004 +0200
@@ -365,7 +365,8 @@
 
 val fast_arith_tac    = Fast_Arith.lin_arith_tac false
 and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
-and trace_arith    = Fast_Arith.trace;
+and trace_arith    = Fast_Arith.trace
+and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
 
 local