src/HOL/Tools/numeral_simprocs.ML

--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 27 07:46:57 2011 +0200
@@ -512,6 +512,7 @@
   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;
 
 (*mult_cancel_left requires a ring with no zero divisors.*)