src/HOL/Tools/numeral_simprocs.ML

--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 28 16:49:15 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Oct 29 10:00:35 2011 +0200
@@ -470,7 +470,6 @@
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
-  val prove_conv = Arith_Data.prove_conv
   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
 end;