--- a/src/FOLP/simp.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/FOLP/simp.ML Fri Nov 21 15:29:56 1997 +0100
@@ -135,7 +135,7 @@
in mk trans_thms end;
(*Applies tactic and returns the first resulting state, FAILS if none!*)
-fun one_result(tac,thm) = case Sequence.pull(tac thm) of
+fun one_result(tac,thm) = case Seq.pull(tac thm) of
Some(thm',_) => thm'
| None => raise THM("Simplifier: could not continue", 0, [thm]);
@@ -211,7 +211,7 @@
| Free _ => resolve_tac congs 1 ORELSE refl1_tac
| _ => refl1_tac)
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
- val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
+ val Some(thm'',_) = Seq.pull(add_norm_tac thm')
in thm'' end;
fun add_norm_tags congs =
@@ -422,7 +422,7 @@
fun simp_lhs(thm,ss,anet,ats,cs) =
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
- else case Sequence.pull(cong_tac i thm) of
+ else case Seq.pull(cong_tac i thm) of
Some(thm',_) =>
let val ps = prems_of thm and ps' = prems_of thm';
val n = length(ps')-length(ps);
@@ -446,7 +446,7 @@
(ss,thm,anet',anet::ats,cs)
end;
-fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
+fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
Some(thm',seq') =>
let val n = (nprems_of thm') - (nprems_of thm)
in pr_rew(i,n,thm,thm',more);
@@ -460,7 +460,7 @@
else (ss,thm,anet,ats,cs);
fun try_true(thm,ss,anet,ats,cs) =
- case Sequence.pull(auto_tac i thm) of
+ case Seq.pull(auto_tac i thm) of
Some(thm',_) => (ss,thm',anet,ats,cs)
| None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
in if !tracing
@@ -471,7 +471,7 @@
end;
fun if_exp(thm,ss,anet,ats,cs) =
- case Sequence.pull (IF1_TAC (cong_tac i) i thm) of
+ case Seq.pull (IF1_TAC (cong_tac i) i thm) of
Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
| None => (ss,thm,anet,ats,cs);
@@ -498,8 +498,8 @@
let val cong_tac = net_tac cong_net
in fn i =>
(fn thm =>
- if i <= 0 orelse nprems_of thm < i then Sequence.null
- else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
+ if i <= 0 orelse nprems_of thm < i then Seq.empty
+ else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
THEN TRY(auto_tac i)
end;
--- a/src/HOL/Modelcheck/MCSyn.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/HOL/Modelcheck/MCSyn.ML Fri Nov 21 15:29:56 1997 +0100
@@ -8,7 +8,7 @@
let val sign = #sign (rep_thm state)
in
case drop(i-1,prems_of state) of
- [] => Sequence.null |
+ [] => Seq.empty |
subgoal::_ =>
let val concl = Logic.strip_imp_concl subgoal;
val OraAss = invoke_oracle MCSyn.thy "mc" (sign,MCOracleExn concl);
--- a/src/HOL/ex/meson.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/HOL/ex/meson.ML Fri Nov 21 15:29:56 1997 +0100
@@ -162,7 +162,7 @@
(*Permits forward proof from rules that discharge assumptions*)
fun forward_res nf st =
- case Sequence.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
+ case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
of Some(th,_) => th
| None => raise THM("forward_res", 0, [st]);
@@ -247,7 +247,7 @@
(METAHYPS (resop (cnf_nil seen)) 1) THEN
(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
+ in Seq.list_of (tac (th RS disj_forward)) @ ths end
and cnf_nil seen th = cnf_aux seen (th,[]);
(*Top-level call to cnf -- it's safe to reset name_ref*)
@@ -270,7 +270,7 @@
(*Forward proof, passing extra assumptions as theorems to the tactic*)
fun forward_res2 nf hyps st =
- case Sequence.pull
+ case Seq.pull
(REPEAT
(METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
st)
@@ -373,7 +373,7 @@
handle INSERT => true;
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
-fun TRYALL_eq_assume_tac 0 st = Sequence.single st
+fun TRYALL_eq_assume_tac 0 st = Seq.single st
| TRYALL_eq_assume_tac i st = TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
handle THM _ => TRYALL_eq_assume_tac (i-1) st;
@@ -381,7 +381,7 @@
-- if *ANY* subgoal has repeated literals*)
fun check_tac st =
if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
- then Sequence.null else Sequence.single st;
+ then Seq.empty else Seq.single st;
(* net_resolve_tac actually made it slower... *)
--- a/src/HOLCF/domain/theorems.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Fri Nov 21 15:29:56 1997 +0100
@@ -28,9 +28,9 @@
| prems=> (cut_facts_tac prems 1)::tacsf);
fun REPEAT_DETERM_UNTIL p tac =
-let fun drep st = if p st then Sequence.single st
- else (case Sequence.pull(tac st) of
- None => Sequence.null
+let fun drep st = if p st then Seq.single st
+ else (case Seq.pull(tac st) of
+ None => Seq.empty
| Some(st',_) => drep st')
in drep end;
val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
--- a/src/Provers/blast.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/Provers/blast.ML Fri Nov 21 15:29:56 1997 +0100
@@ -459,7 +459,7 @@
(*Like dup_elim, but puts the duplicated major premise FIRST*)
-fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd;
+fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;
(*Count new hyps so that they can be rotated*)
@@ -467,10 +467,10 @@
| nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
| nNewHyps (P::Ps) = 1 + nNewHyps Ps;
-fun rot_subgoals_tac [] i st = Sequence.single st
+fun rot_subgoals_tac [] i st = Seq.single st
| rot_subgoals_tac (k::ks) i st =
- rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st))
- handle OPTION => Sequence.null;
+ rot_subgoals_tac ks (i+1) (Seq.hd (rotate_tac (~k) i st))
+ handle OPTION => Seq.empty;
fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
@@ -1166,17 +1166,17 @@
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
fun cont (tacs,_,choices) =
- (case Sequence.pull(EVERY' (rev tacs) i st) of
+ (case Seq.pull(EVERY' (rev tacs) i st) of
None => (writeln ("PROOF FAILED for depth " ^
Int.toString lim);
backtrack choices)
- | cell => Sequence.seqof(fn()=> cell))
+ | cell => Seq.make(fn()=> cell))
in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
end
- handle PROVE => Sequence.null);
+ handle PROVE => Seq.empty);
fun blast_tac cs i st = (DEEPEN (1,20) (depth_tac cs) 0) i st
- handle TRANS s => (warning ("Blast_tac: " ^ s); Sequence.null);
+ handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
fun Blast_tac i = blast_tac (Data.claset()) i;
--- a/src/Provers/classical.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/Provers/classical.ML Fri Nov 21 15:29:56 1997 +0100
@@ -201,7 +201,7 @@
(*Duplication of hazardous rules, for complete provers*)
fun dup_intr th = zero_var_indexes (th RS classical);
-fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |>
+fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |>
rule_by_tactic (TRYALL (etac revcut_rl));
--- a/src/Provers/simp.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/Provers/simp.ML Fri Nov 21 15:29:56 1997 +0100
@@ -129,7 +129,7 @@
in mk trans_thms end;
(*Applies tactic and returns the first resulting state, FAILS if none!*)
-fun one_result(tac,thm) = case Sequence.pull(tac thm) of
+fun one_result(tac,thm) = case Seq.pull(tac thm) of
Some(thm',_) => thm'
| None => raise THM("Simplifier: could not continue", 0, [thm]);
@@ -205,7 +205,7 @@
| Free _ => resolve_tac congs 1 ORELSE refl1_tac
| _ => refl1_tac))
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
- val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
+ val Some(thm'',_) = Seq.pull(add_norm_tac thm')
in thm'' end;
fun add_norm_tags congs =
@@ -443,7 +443,7 @@
fun simp_lhs(thm,ss,anet,ats,cs) =
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
- else case Sequence.pull(cong_tac i thm) of
+ else case Seq.pull(cong_tac i thm) of
Some(thm',_) =>
let val ps = prems_of thm and ps' = prems_of thm';
val n = length(ps')-length(ps);
@@ -467,7 +467,7 @@
(ss,thm,anet',anet::ats,cs)
end;
-fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
+fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
Some(thm',seq') =>
let val n = (nprems_of thm') - (nprems_of thm)
in pr_rew(i,n,thm,thm',more);
@@ -481,7 +481,7 @@
else (ss,thm,anet,ats,cs);
fun try_true(thm,ss,anet,ats,cs) =
- case Sequence.pull(auto_tac i thm) of
+ case Seq.pull(auto_tac i thm) of
Some(thm',_) => (ss,thm',anet,ats,cs)
| None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
in if !tracing
@@ -492,7 +492,7 @@
end;
fun split(thm,ss,anet,ats,cs) =
- case Sequence.pull(tapply(split_tac
+ case Seq.pull(tapply(split_tac
(cong_tac i,splits,split_consts) i,thm)) of
Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs)
| None => (ss,thm,anet,ats,cs);
--- a/src/Provers/simplifier.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/Provers/simplifier.ML Fri Nov 21 15:29:56 1997 +0100
@@ -346,7 +346,7 @@
fun simp mode (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) thm =
let
val tacf = solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
- fun prover m th = apsome fst (Sequence.pull (tacf m th));
+ fun prover m th = apsome fst (Seq.pull (tacf m th));
in
Drule.rewrite_thm mode prover mss thm
end;
--- a/src/ZF/ROOT.ML Fri Nov 21 15:27:43 1997 +0100
+++ b/src/ZF/ROOT.ML Fri Nov 21 15:29:56 1997 +0100
@@ -15,11 +15,11 @@
(*For Pure/tactic?? A crude way of adding structure to rules*)
fun CHECK_SOLVED tac st =
- case Sequence.pull (tac st) of
+ case Seq.pull (tac st) of
None => error"DO_GOAL: tactic list failed"
| Some(x,_) =>
if has_fewer_prems 1 x then
- Sequence.cons(x, Sequence.null)
+ Seq.cons(x, Seq.empty)
else (writeln"DO_GOAL: unsolved goals!!";
writeln"Final proof state was ...";
print_goals (!goals_limit) x;