| changeset 7570 | a9391550eea1 |
| parent 6919 | 7985b229806c |
| child 9517 | f58863b1406a |
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML Tue Sep 21 19:10:39 1999 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML Tue Sep 21 19:11:07 1999 +0200 @@ -28,7 +28,7 @@ let val (cs,ss) = MI_css in - (cs addSEs [squareE], ss addSSolver (fn thms => assume_tac ORELSE' (etac notE))) + (cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE)))) end; val temp_elim = make_elim o temp_use;