--- a/ProgTutorial/Solutions.thy	Mon Mar 30 08:17:22 2009 +0000
+++ b/ProgTutorial/Solutions.thy	Mon Mar 30 09:33:50 2009 +0100
@@ -65,7 +65,7 @@
   val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
   val goal = Logic.mk_equals (t, sum)
 in
-  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
+  Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
 end
 
 fun add_sp_aux ss t =