diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/Tactical.thy	Sat Aug 28 13:27:16 2010 +0800
@@ -1912,7 +1912,7 @@
   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
   (therefore we printing it out using the function @{ML pretty_term in Pretty}).
   We can turn this function into a proper simproc using the function 
-  @{ML Simplifier.simproc_i}:
+  @{ML Simplifier.simproc_global_i}:
 *}
 
 
@@ -1921,7 +1921,7 @@
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
 in
-  Simplifier.simproc_i thy "fail_simproc'" pat (K fail_simproc')
+  Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc')
 end*}
 
 text {*
@@ -1978,7 +1978,7 @@
   val thy = @{theory}
   val pat = [@{term "Suc n"}] 
 in
-  Simplifier.simproc_i thy "sproc +1" pat (K plus_one_simproc)
+  Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc)
 end*}
 
 text {*
@@ -2086,7 +2086,7 @@
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
 in 
-  Simplifier.simproc_i thy "nat_number" pat (K nat_number_simproc) 
+  Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc) 
 end*}
 
 text {*