--- a/ProgTutorial/Essential.thy	Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Essential.thy	Wed Feb 23 23:55:37 2011 +0000
@@ -1704,7 +1704,7 @@
   val thm = @{thm foo_test1}
   val meta_eq = Object_Logic.atomize (cprop_of thm)
 in
-  MetaSimplifier.rewrite_rule [meta_eq] thm
+  Raw_Simplifier.rewrite_rule [meta_eq] thm
 end"
   "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 
@@ -1728,7 +1728,7 @@
   val thm' = forall_intr_vars thm
   val thm'' = Object_Logic.atomize (cprop_of thm')
 in
-  MetaSimplifier.rewrite_rule [thm''] thm'
+  Raw_Simplifier.rewrite_rule [thm''] thm'
 end*}
 
 text {*