Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Memory/MemoryImplementation.thy
changeset 32149 ef59550a55d3
parent 27208 5fe899199f85
child 36866 426d5781bb25 
--- 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
isabelle