--- a/ProgTutorial/First_Steps.thy	Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/First_Steps.thy	Wed Feb 23 23:55:37 2011 +0000
@@ -158,34 +158,6 @@
 
   @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 
-  It is also possible to redirect the ``channel'' where the string @{text
-  "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from
-  choking on massive amounts of trace output. This redirection can be achieved
-  with the code:
-*}
-
-ML{*val strip_specials =
-let
-  fun strip ("\^A" :: _ :: cs) = strip cs
-    | strip (c :: cs) = c :: strip cs
-    | strip [] = [];
-in 
-  implode o strip o explode 
-end
-
-fun redirect_tracing stream =
- Output.Private_Hooks.tracing_fn := (fn s =>
-    (TextIO.output (stream, (strip_specials s));
-     TextIO.output (stream, "\n");
-     TextIO.flushOut stream)) *}
-
-text {*
-  Calling now
-
-  @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"}
-
-  will cause that all tracing information is printed into the file @{text "foo.bar"}.
-
   You can print out error messages with the function @{ML_ind error in Library}; for 
   example:
 
@@ -900,13 +872,13 @@
 
 ML{*fun get_thm_names_from_ss simpset =
 let
-  val {simps,...} = MetaSimplifier.dest_ss simpset
+  val {simps,...} = Raw_Simplifier.dest_ss simpset
 in
   map #1 simps
 end*}
 
 text {*
-  The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all
+  The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all
   information stored in the simpset, but here we are only interested in the names of the
   simp-rules. Now you can feed in the current simpset into this function. 
   The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.