--- a/ProgTutorial/Tactical.thy	Sat Oct 10 15:16:44 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat Oct 10 18:25:43 2009 +0200
@@ -1246,7 +1246,7 @@
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
-  val {simps, congs, procs, ...} = Simplifier.dest_ss ss
+  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
       "  " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm)
@@ -1263,7 +1263,7 @@
 text_raw {* 
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML_ind  dest_ss in Simplifier} returns a record containing
+\caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}