--- 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 {*