diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Feb 23 23:55:37 2011 +0000
@@ -1400,7 +1400,7 @@
   corresponding preconditions.
 
   \begin{readmore}
-  For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
+  For more information about the simplifier see @{ML_file "Pure/raw_simplifier.ML"}
   and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in 
   @{ML_file "Provers/splitter.ML"}.
   \end{readmore}
@@ -1413,9 +1413,9 @@
 
   \begin{isabelle}
   \begin{tabular}{l@ {\hspace{10mm}}l}
-  @{ML_ind addsimps in MetaSimplifier}    & @{ML_ind delsimps in MetaSimplifier}\\
-  @{ML_ind addcongs in MetaSimplifier}    & @{ML_ind delcongs in MetaSimplifier}\\
-  @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\
+  @{ML_ind addsimps in Raw_Simplifier}    & @{ML_ind delsimps in Raw_Simplifier}\\
+  @{ML_ind addcongs in Raw_Simplifier}    & @{ML_ind delcongs in Raw_Simplifier}\\
+  @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\
   \end{tabular}
   \end{isabelle}
 
@@ -1428,7 +1428,7 @@
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
-  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+  val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
     Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
@@ -1445,7 +1445,7 @@
 text_raw {* 
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing
+\caption{The function @{ML_ind dest_ss in Raw_Simplifier} 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} *}
@@ -1454,7 +1454,7 @@
 text {* 
   To see how they work, consider the function in Figure~\ref{fig:printss}, which
   prints out some parts of a simpset. If you use it to print out the components of the
-  empty simpset, i.e., @{ML_ind empty_ss in MetaSimplifier}
+  empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
   
   @{ML_response_fake [display,gray]
   "print_ss @{context} empty_ss"
@@ -1559,7 +1559,7 @@
   \end{readmore}
 
   The simplifier is often used to unfold definitions in a proof. For this the
-  simplifier implements the tactic @{ML_ind rewrite_goal_tac in MetaSimplifier}.\footnote{\bf FIXME: 
+  simplifier implements the tactic @{ML_ind rewrite_goal_tac in Raw_Simplifier}.\footnote{\bf FIXME: 
   see LocalDefs infrastructure.} Suppose for example the
   definition
 *}
@@ -1581,7 +1581,7 @@
 
 text {*
   If you want to unfold definitions in \emph{all} subgoals, not just one, 
-  then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}.
+  then use the the tactic @{ML_ind rewrite_goals_tac in Raw_Simplifier}.
 *}
 
 
@@ -1871,7 +1871,7 @@
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
   The function also takes a list of patterns that can trigger the simproc.
   Now the simproc is set up and can be explicitly added using
-  @{ML_ind addsimprocs in MetaSimplifier} to a simpset whenever
+  @{ML_ind addsimprocs in Raw_Simplifier} to a simpset whenever
   needed. 
 
   Simprocs are applied from inside to outside and from left to right. You can
@@ -2539,7 +2539,7 @@
   See @{ML_file "Pure/conv.ML"}
   for more information about conversion combinators. 
   Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
-  @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
+  @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/raw_simplifier.ML"}.
   \end{readmore}
 
 *}