src/Sequents/prover.ML

--- a/src/Sequents/prover.ML	Tue Jul 22 11:12:55 1997 +0200
+++ b/src/Sequents/prover.ML	Tue Jul 22 11:14:18 1997 +0200
@@ -85,13 +85,13 @@
 
 fun RESOLVE_THEN rules =
   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
-      fun tac nextac i = STATE (fn state =>  
-	  filseq_resolve_tac rls0 9999 i 
-	  ORELSE
-	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
-	  ORELSE
-	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
-					THEN  TRY(nextac i)) )
+      fun tac nextac i state = state |>
+	     (filseq_resolve_tac rls0 9999 i 
+	      ORELSE
+	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
+	      ORELSE
+	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
+					    THEN  TRY(nextac i)))
   in  tac  end;
 
 
@@ -202,11 +202,11 @@
 
 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
                                     else tf(i) THEN tac(i-1)
-                    in STATE(fn state=> tac(nprems_of state)) end;
+                    in fn st => tac (nprems_of st) st end;
 
 (* Depth first search bounded by d *)
-fun solven_tac d n = STATE (fn state =>
-        if d<0 then no_tac
+fun solven_tac d n state = state |>
+       (if d<0 then no_tac
         else if (nprems_of state = 0) then all_tac 
         else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
                  ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
@@ -214,10 +214,10 @@
 
 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
 
-fun step_tac n = STATE (fn state =>  
-      if (nprems_of state = 0) then all_tac 
-      else (DETERM(fres_safe_tac n)) ORELSE 
-           (fres_unsafe_tac n APPEND fres_bound_tac n));
+fun step_tac n = 
+    COND (has_fewer_prems 1) all_tac 
+         (DETERM(fres_safe_tac n) ORELSE 
+	  (fres_unsafe_tac n APPEND fres_bound_tac n));
 
 end;
 end;