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