--- a/ProgTutorial/First_Steps.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/First_Steps.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -842,8 +842,9 @@
   simpset.
 *}
 
-ML %grayML{*fun get_thm_names_from_ss simpset =
+ML %grayML{*fun get_thm_names_from_ss ctxt =
 let
+  val simpset = Raw_Simplifier.simpset_of ctxt
   val {simps,...} = Raw_Simplifier.dest_ss simpset
 in
   map #1 simps
@@ -853,10 +854,10 @@
   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}"}.
+  The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
 
   @{ML_response_fake [display,gray] 
-  "get_thm_names_from_ss @{simpset}" 
+  "get_thm_names_from_ss @{context}" 
   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
   Again, this way of referencing simpsets makes you independent from additions