diff -r d5db6dfcb34a -r 32d498cf7595 src/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOLCF/IOA/NTP/Impl.thy	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Tue Nov 18 18:25:42 2008 +0100
@@ -220,7 +220,7 @@
     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
 
   apply (tactic "tac2 1")
-  apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}]
+  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
     (@{thm Impl.hdr_sum_def})] *})
   apply arith
 
@@ -238,7 +238,7 @@
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   apply (intro strip)
   apply (erule conjE)+
-  apply (tactic {* fold_tac  [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   apply simp
 
   done