# HG changeset patch
# User wenzelm
# Date 880122596 -3600
# Node ID 3a82492e70c52ce8d9865f0569ea5d94d1eb070e
# Parent  957c887b89b59e0e6318e793d56bd48f2b7717e7
changed Pure/Sequence interface -- isatool fixseq;

diff -r 957c887b89b5 -r 3a82492e70c5 src/FOLP/simp.ML
--- 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;
 
diff -r 957c887b89b5 -r 3a82492e70c5 src/HOL/Modelcheck/MCSyn.ML
--- 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);
diff -r 957c887b89b5 -r 3a82492e70c5 src/HOL/ex/meson.ML
--- 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... *)
diff -r 957c887b89b5 -r 3a82492e70c5 src/HOLCF/domain/theorems.ML
--- 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);
diff -r 957c887b89b5 -r 3a82492e70c5 src/Provers/blast.ML
--- 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;
 
diff -r 957c887b89b5 -r 3a82492e70c5 src/Provers/classical.ML
--- 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));
 
 
diff -r 957c887b89b5 -r 3a82492e70c5 src/Provers/simp.ML
--- 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);
diff -r 957c887b89b5 -r 3a82492e70c5 src/Provers/simplifier.ML
--- 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;
diff -r 957c887b89b5 -r 3a82492e70c5 src/ZF/ROOT.ML
--- 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;