src/Sequents/prover.ML
changeset 3538 ed9de44032e0
parent 2073 fb0655539d05
child 3948 3428c0a88449
     1.1 --- a/src/Sequents/prover.ML	Tue Jul 22 11:12:55 1997 +0200
     1.2 +++ b/src/Sequents/prover.ML	Tue Jul 22 11:14:18 1997 +0200
     1.3 @@ -85,13 +85,13 @@
     1.4  
     1.5  fun RESOLVE_THEN rules =
     1.6    let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
     1.7 -      fun tac nextac i = STATE (fn state =>  
     1.8 -	  filseq_resolve_tac rls0 9999 i 
     1.9 -	  ORELSE
    1.10 -	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    1.11 -	  ORELSE
    1.12 -	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    1.13 -					THEN  TRY(nextac i)) )
    1.14 +      fun tac nextac i state = state |>
    1.15 +	     (filseq_resolve_tac rls0 9999 i 
    1.16 +	      ORELSE
    1.17 +	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    1.18 +	      ORELSE
    1.19 +	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    1.20 +					    THEN  TRY(nextac i)))
    1.21    in  tac  end;
    1.22  
    1.23  
    1.24 @@ -202,11 +202,11 @@
    1.25  
    1.26  fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
    1.27                                      else tf(i) THEN tac(i-1)
    1.28 -                    in STATE(fn state=> tac(nprems_of state)) end;
    1.29 +                    in fn st => tac (nprems_of st) st end;
    1.30  
    1.31  (* Depth first search bounded by d *)
    1.32 -fun solven_tac d n = STATE (fn state =>
    1.33 -        if d<0 then no_tac
    1.34 +fun solven_tac d n state = state |>
    1.35 +       (if d<0 then no_tac
    1.36          else if (nprems_of state = 0) then all_tac 
    1.37          else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
    1.38                   ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
    1.39 @@ -214,10 +214,10 @@
    1.40  
    1.41  fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
    1.42  
    1.43 -fun step_tac n = STATE (fn state =>  
    1.44 -      if (nprems_of state = 0) then all_tac 
    1.45 -      else (DETERM(fres_safe_tac n)) ORELSE 
    1.46 -           (fres_unsafe_tac n APPEND fres_bound_tac n));
    1.47 +fun step_tac n = 
    1.48 +    COND (has_fewer_prems 1) all_tac 
    1.49 +         (DETERM(fres_safe_tac n) ORELSE 
    1.50 +	  (fres_unsafe_tac n APPEND fres_bound_tac n));
    1.51  
    1.52  end;
    1.53  end;