src/HOL/TLA/Memory/MemoryImplementation.thy

 *)
 ML {*
   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);
 *}
 
 setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}