diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun May 15 17:45:53 2011 +0200
@@ -803,7 +803,7 @@
 method_setup split_idle = {*
   Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
     >> (K (SIMPLE_METHOD' o split_idle_tac))
-*} ""
+*}
 
 (* ----------------------------------------------------------------------
    Combine steps 1.2 and 1.4 to prove that the implementation satisfies