src/HOL/TLA/Memory/MemoryImplementation.thy

--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -227,7 +227,7 @@
   val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
   val fast_solver = mk_solver "fast_solver" (fn ctxt =>
     if Config.get ctxt config_fast_solver
-    then assume_tac ORELSE' (etac notE)
+    then assume_tac ctxt ORELSE' (etac notE)
     else K no_tac);
 *}