--- a/ProgTutorial/Essential.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Essential.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -1605,7 +1605,7 @@
   "let
   fun pred s = match_string \"my_thm_simp\" s
 in
-  exists pred (get_thm_names_from_ss @{simpset})
+  exists pred (get_thm_names_from_ss @{context})
 end"
   "true"}
 
@@ -1899,7 +1899,7 @@
   \begin{readmore}
   Functions that setup goal states and prove theorems are implemented in 
   @{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to
-  skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}.
+  skip proofs of theorems are implemented in @{ML_file "Pure/skip_proof.ML"}.
   \end{readmore}
 
   Theorems also contain auxiliary data, such as the name of the theorem, its