src/Sequents/prover.ML
 changeset 3538 ed9de44032e0 parent 2073 fb0655539d05 child 3948 3428c0a88449
```--- 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;```