src/HOL/ex/meson.ML

--- a/src/HOL/ex/meson.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/HOL/ex/meson.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -245,8 +245,8 @@
   handle THM _ => (*disjunction?*)
     let val tac = 
         (METAHYPS (resop (cnf_nil seen)) 1) THEN
-        (STATE (fn st' => 
-                METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))
+        (fn st' => st' |>
+                METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
     in  Sequence.list_of_s (tac (th RS disj_forward)) @ ths  end
 and cnf_nil seen th = cnf_aux seen (th,[]);