--- a/ProgTutorial/Tactical.thy	Mon May 17 17:27:21 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Mon May 17 18:20:48 2010 +0100
@@ -2262,7 +2262,7 @@
   "True \<or> P \<equiv> True \<or> P"}
 
   Rewriting with more than one theorem can be done using the function 
-  @{ML_ind rewrs_conv in More_Conv} from the structure @{ML_struct More_Conv}.
+  @{ML_ind rewrs_conv in Conv} from the structure @{ML_struct Conv}.
   
 
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
@@ -2345,21 +2345,21 @@
 text {*
   Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
   implemented more succinctly with the combinators @{ML_ind bottom_conv in
-  More_Conv} and @{ML_ind top_conv in More_Conv}. For example:
+  Conv} and @{ML_ind top_conv in Conv}. For example:
 *}
 
 ML{*fun true_conj1_conv ctxt =
 let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
 in
-  More_Conv.bottom_conv (K conv) ctxt
+  Conv.bottom_conv (K conv) ctxt
 end*}
 
 text {*
   If we regard terms as trees with variables and constants on the top, then 
-  @{ML bottom_conv in More_Conv} traverses first the the term and
+  @{ML bottom_conv in Conv} traverses first the the term and
   on the ``way down'' applies the conversion, whereas @{ML top_conv in
-  More_Conv} applies the conversion on the ``way up''. To see the difference, 
+  Conv} applies the conversion on the ``way up''. To see the difference, 
   assume the following two meta-equations
 *}
 
@@ -2378,9 +2378,9 @@
   @{ML_response_fake [display, gray]
   "let
   val ctxt = @{context}
-  val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
-  val conv_top = More_Conv.top_conv (K conv) ctxt
-  val conv_bot = More_Conv.bottom_conv (K conv) ctxt
+  val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
+  val conv_top = Conv.top_conv (K conv) ctxt
+  val conv_bot = Conv.bottom_conv (K conv) ctxt
   val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
 in
   (conv_top ctrm, conv_bot ctrm)
@@ -2400,13 +2400,13 @@
       Conv.arg_conv (true_conj1_conv ctxt) ctrm
   | _ => Conv.no_conv ctrm 
 
-val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*}
+val if_true1_conv = Conv.top_sweep_conv if_true1_simple_conv*}
 
 text {*
   In the first function we only treat the top-most redex and also only the
   success case. As default we return @{ML no_conv in Conv}.  To apply this
   ``simple'' conversion inside a term, we use in the last line the combinator @{ML_ind
-  top_sweep_conv in More_Conv}, which traverses the term starting from the
+  top_sweep_conv in Conv}, which traverses the term starting from the
   root and applies it to all the redexes on the way, but stops in each branch as
   soon as it found one redex. Here is an example for this conversion:
 
@@ -2496,7 +2496,7 @@
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
   the conclusion according to @{ML true_conj1_conv}. If we only have one
   conversion that should be uniformly applied to the whole goal state, we
-  can simplify @{ML true1_tac} using @{ML_ind top_conv in More_Conv}.
+  can simplify @{ML true1_tac} using @{ML_ind top_conv in Conv}.
 
   Conversions are also be helpful for constructing meta-equality theorems.
   Such theorems are often definitions. As an example consider the following
@@ -2592,7 +2592,7 @@
   \end{exercise}
 
   \begin{readmore}
-  See @{ML_file "Pure/conv.ML"} and  @{ML_file "Tools/more_conv.ML"}
+  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"}.