| changeset 43596 | 78211f66cf8d |
| parent 42814 | 5af15f1e2ef6 |
| child 45133 | 2214ba5bdfff |
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Jun 29 20:39:41 2011 +0200 @@ -225,7 +225,7 @@ *) ML {* val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); - val fast_solver = mk_solver' "fast_solver" (fn ss => + val fast_solver = mk_solver "fast_solver" (fn ss => if Config.get (Simplifier.the_context ss) config_fast_solver then assume_tac ORELSE' (etac notE) else K no_tac);