src/HOL/Tools/nat_numeral_simprocs.ML

--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Oct 27 07:46:57 2011 +0200
@@ -366,6 +366,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;
 
 structure EqCancelFactor = ExtractCommonTermFun