
diff -r 253f6808dabe -r ef59550a55d3 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -763,7 +763,7 @@
 *)
 ML {*
 fun split_idle_tac ctxt simps i =
-  let val ss = Simplifier.local_simpset_of ctxt in
+  let val ss = simpset_of ctxt in
     TRY (rtac @{thm actionI} i) THEN
     InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
     rewrite_goals_tac @{thms action_rews} THEN




