--- a/CookBook/Solutions.thy	Mon Feb 23 00:27:27 2009 +0000
+++ b/CookBook/Solutions.thy	Mon Feb 23 17:08:15 2009 +0000
@@ -63,9 +63,9 @@
 fun get_sum_thm ctxt t (n1, n2) =  
 let 
   val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
-  val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, sum))
+  val goal = Logic.mk_equals (t, sum)
 in
-  mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
 end
 
 fun add_sp_aux ss t =