diff -r 19b47bfac6ef -r 9e7d1c139569 src/Doc/IsarImplementation/Isar.thy
--- a/src/Doc/IsarImplementation/Isar.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/Doc/IsarImplementation/Isar.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -385,7 +385,7 @@
   Attrib.thms >> (fn thms => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
       CHANGED (asm_full_simp_tac
-        (HOL_basic_ss addsimps thms) i)))
+        (put_simpset HOL_basic_ss ctxt addsimps thms) i)))
 *} "rewrite subgoal by given rules"
 
 text {* The concrete syntax wrapping of @{command method_setup} always
@@ -424,7 +424,7 @@
     SIMPLE_METHOD
       (CHANGED
         (ALLGOALS (asm_full_simp_tac
-          (HOL_basic_ss addsimps thms)))))
+          (put_simpset HOL_basic_ss ctxt addsimps thms)))))
 *} "rewrite all subgoals by given rules"
 
 notepad
@@ -458,7 +458,8 @@
   Attrib.thms >> (fn thms => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
       CHANGED (asm_full_simp_tac
-        (HOL_basic_ss addsimps (thms @ My_Simps.get ctxt)) i)))
+        (put_simpset HOL_basic_ss ctxt
+          addsimps (thms @ My_Simps.get ctxt)) i)))
 *} "rewrite subgoal by given rules and my_simp rules from the context"
 
 text {*