# HG changeset patch
# User wenzelm
# Date 880122463 -3600
# Node ID 957c887b89b59e0e6318e793d56bd48f2b7717e7
# Parent  a045600f0c9861d5e247435818b8f31dafa27420
changed Sequence interface (now Seq, in seq.ML);

diff -r a045600f0c98 -r 957c887b89b5 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/IsaMakefile	Fri Nov 21 15:27:43 1997 +0100
@@ -19,7 +19,7 @@
 	Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \
 	axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
 	goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
-	pattern.ML pure_thy.ML search.ML section_utils.ML sequence.ML sign.ML \
+	pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \
 	sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
 	type.ML type_infer.ML unify.ML
 
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/ROOT.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -27,7 +27,7 @@
 use "type_infer.ML";
 use "type.ML";
 use "sign.ML";
-use "sequence.ML";
+use "seq.ML";
 use "envir.ML";
 use "pattern.ML";
 use "unify.ML";
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/display.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -24,7 +24,7 @@
   val print_data	: theory -> string -> unit
   val print_thm		: thm -> unit
   val prth		: thm -> thm
-  val prthq		: thm Sequence.seq -> thm Sequence.seq
+  val prthq		: thm Seq.seq -> thm Seq.seq
   val prths		: thm list -> thm list
   val show_hyps		: bool ref
   val string_of_cterm	: cterm -> string
@@ -67,7 +67,7 @@
 
 (*Print and return a sequence of theorems, separated by blank lines. *)
 fun prthq thseq =
-  (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
+  (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
 
 (*Print and return a list of theorems, separated by blank lines. *)
 fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths);
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/drule.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -256,7 +256,7 @@
 
 (*Resolution: exactly one resolvent must be produced.*)
 fun tha RSN (i,thb) =
-  case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
+  case Seq.chop (2, biresolution false [(false,tha)] i thb) of
       ([th],_) => th
     | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
@@ -267,7 +267,7 @@
 (*For joining lists of rules*)
 fun thas RLN (i,thbs) =
   let val resolve = biresolution false (map (pair false) thas) i
-      fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
+      fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
   in  List.concat (map resb thbs)  end;
 
 fun thas RL thbs = thas RLN (1,thbs);
@@ -289,7 +289,7 @@
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)
 fun compose(tha,i,thb) =
-    Sequence.list_of_s (bicompose false (false,tha,0) i thb);
+    Seq.list_of (bicompose false (false,tha,0) i thb);
 
 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
 fun tha COMP thb =
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/goals.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -76,7 +76,7 @@
 
 (*Each level of goal stack includes a proof state and alternative states,
   the output of the tactic applied to the preceeding level.  *)
-type gstack = (thm * thm Sequence.seq) list;
+type gstack = (thm * thm Seq.seq) list;
 
 datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
 
@@ -101,7 +101,7 @@
 
 (*List of previous goal stacks, for the undo operation.  Set by setstate. 
   A list of lists!*)
-val undo_list = ref([[(dummy, Sequence.null)]] : gstack list);
+val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
 
 (* Stack of proof attempts *)
 val proofstack = ref([]: proof list);
@@ -137,7 +137,7 @@
       (*discharges assumptions from state in the order they appear in goal;
 	checks (if requested) that resulting theorem is equivalent to goal. *)
       fun mkresult (check,state) =
-        let val state = Sequence.hd (flexflex_rule state)
+        let val state = Seq.hd (flexflex_rule state)
 	    		handle THM _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
             val th = strip_shyps (implies_intr_list cAs state)
@@ -199,7 +199,7 @@
   let val (prems, st0, mkresult) = prepare_proof rths chorn
       val tac = EVERY (tacsf prems)
       fun statef() = 
-	  (case Sequence.pull (tac st0) of 
+	  (case Seq.pull (tac st0) of 
 	       Some(st,_) => st
 	     | _ => error ("prove_goal: tactic failed"))
   in  mkresult (true, cond_timeit (!proof_timing) statef)  end
@@ -243,7 +243,7 @@
   !print_current_goals_fn (length pairs) (!goals_limit) th;
 
 (*Printing can raise exceptions, so the assignment occurs last.
-  Can do   setstate[(st,Sequence.null)]  to set st as the state.  *)
+  Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
 fun setstate newgoals = 
   (print_top (pop newgoals);  undo_list := newgoals :: !undo_list);
 
@@ -307,7 +307,7 @@
 fun goalw_cterm rths chorn = 
   let val (prems, st0, mkresult) = prepare_proof rths chorn
   in  undo_list := [];
-      setstate [ (st0, Sequence.null) ];  
+      setstate [ (st0, Seq.empty) ];  
       curr_prems := prems;
       curr_mkresult := mkresult;
       prems
@@ -324,7 +324,7 @@
 
 (*Proof step "by" the given tactic -- apply tactic to the proof state*)
 fun by_com tac ((th,ths), pairs) : gstack =
-  (case  Sequence.pull(tac th)  of
+  (case  Seq.pull(tac th)  of
      None      => error"by: tactic failed"
    | Some(th2,ths2) => 
        (if eq_thm(th,th2) 
@@ -346,7 +346,7 @@
   If none at this level, try earlier levels*)
 fun backtrack [] = error"back: no alternatives"
   | backtrack ((th,thstr) :: pairs) =
-     (case Sequence.pull thstr of
+     (case Seq.pull thstr of
 	  None      => (writeln"Going back a level..."; backtrack pairs)
 	| Some(th2,thstr2) =>  
 	   (if eq_thm(th,th2) 
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/search.ML
--- a/src/Pure/search.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/search.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -47,14 +47,14 @@
  let val tac = tracify trace_DEPTH_FIRST tac
      fun depth used [] = None
        | depth used (q::qs) =
-	  case Sequence.pull q of
+	  case Seq.pull q of
 	      None         => depth used qs
 	    | Some(st,stq) => 
 		if satp st andalso not (gen_mem eq_thm (st, used))
-		then Some(st, Sequence.seqof
+		then Some(st, Seq.make
 			         (fn()=> depth (st::used) (stq::qs)))
 		else depth used (tac st :: stq :: qs)
-  in  traced_tac (fn st => depth [] ([Sequence.single st]))  end;
+  in  traced_tac (fn st => depth [] ([Seq.single st]))  end;
 
 
 
@@ -136,11 +136,11 @@
 		    writeln (string_of_int np ^ 
 			     implode (map (fn _ => "*") qs))
 		else ();
-		Sequence.pull q) of
+		Seq.pull q) of
 	     None         => depth (bnd,inc) qs
 	   | Some(st,stq) => 
 	       if satp st	(*solution!*)
-	       then Some(st, Sequence.seqof
+	       then Some(st, Seq.make
 			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
 
 	       else 
@@ -185,7 +185,7 @@
 
 (*For creating output sequence*)
 fun some_of_list []     = None
-  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
+  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
 
 
 (*Best-first search for a state that satisfies satp (incl initial state)
@@ -205,8 +205,8 @@
 	       then writeln("state size = " ^ string_of_int n ^ 
 		         "  queue length =" ^ string_of_int (length nprfs))  
                else ();
-	     bfs (Sequence.list_of_s (tac prf), nprfs))
-      fun btac st = bfs (Sequence.list_of_s (tac0 st),  [])
+	     bfs (Seq.list_of (tac prf), nprfs))
+      fun btac st = bfs (Seq.list_of (tac0 st),  [])
   in traced_tac btac end;
 
 (*Ordinary best-first search, with no initial tactic*)
@@ -215,7 +215,7 @@
 (*Breadth-first search to satisfy satpred (including initial state) 
   SLOW -- SHOULD NOT USE APPEND!*)
 fun BREADTH_FIRST satpred tac = 
-  let val tacf = Sequence.list_of_s o tac;
+  let val tacf = Seq.list_of o tac;
       fun bfs prfs =
 	 (case  partition satpred prfs  of
 	      ([],[]) => []
@@ -223,7 +223,7 @@
 		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
 		   bfs (List.concat (map tacf nonsats)))
 	    | (sats,_)  => sats)
-  in (fn st => Sequence.s_of_list (bfs [st])) end;
+  in (fn st => Seq.of_list (bfs [st])) end;
 
 
 (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
@@ -242,7 +242,7 @@
 
 (*For creating output sequence*)
 fun some_of_list []     = None
-  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
+  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
 
 val trace_ASTAR = ref false; 
 
@@ -262,8 +262,8 @@
 			 "  cost = " ^ string_of_int n ^ 
                          "  queue length =" ^ string_of_int (length nprfs))  
                else ();
-             bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
-      fun tf st = bfs (Sequence.list_of_s (tac0 st), [], 0)
+             bfs (Seq.list_of (tf prf), nprfs,level+1))
+      fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
   in traced_tac tf end;
 
 (*Ordinary ASTAR, with no initial tactic*)
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/seq.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/seq.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -0,0 +1,155 @@
+(*  Title:      Pure/seq.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Unbounded sequences implemented by closures.  RECOMPUTES if sequence
+is re-inspected.  Memoing, using polymorphic refs, was found to be
+slower!  (More GCs)
+*)
+
+signature SEQ =
+sig
+  type 'a seq
+  val make: (unit -> ('a * 'a seq) option) -> 'a seq
+  val pull: 'a seq -> ('a * 'a seq) option
+  val empty: 'a seq
+  val cons: 'a * 'a seq -> 'a seq
+  val single: 'a -> 'a seq
+  val hd: 'a seq -> 'a
+  val tl: 'a seq -> 'a seq
+  val chop: int * 'a seq -> 'a list * 'a seq
+  val list_of: 'a seq -> 'a list
+  val of_list: 'a list -> 'a seq
+  val map: ('a -> 'b) -> 'a seq -> 'b seq
+  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
+  val append: 'a seq * 'a seq -> 'a seq
+  val filter: ('a -> bool) -> 'a seq -> 'a seq
+  val flat: 'a seq seq -> 'a seq
+  val interleave: 'a seq * 'a seq -> 'a seq
+  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
+  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+end;
+
+structure Seq: SEQ =
+struct
+
+
+datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
+
+(*the abstraction for making a sequence*)
+val make = Seq;
+
+(*return next sequence element as None or Some (x, xq)*)
+fun pull (Seq f) = f ();
+
+
+(*the empty sequence*)
+val empty = make (fn () => None);
+
+(*prefix an element to the sequence -- use cons (x, xq) only if
+  evaluation of xq need not be delayed, otherwise use
+  make (fn () => Some (x, xq))*)
+fun cons x_xq = make (fn () => Some x_xq);
+
+fun single x = cons (x, empty);
+
+(*head and tail -- beware of calling the sequence function twice!!*)
+fun hd xq = #1 (the (pull xq))
+and tl xq = #2 (the (pull xq));
+
+
+(*the list of the first n elements, paired with rest of sequence;
+  if length of list is less than n, then sequence had less than n elements*)
+fun chop (n, xq) =
+  if n <= 0 then ([], xq)
+  else
+    (case pull xq of
+      None => ([], xq)
+    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
+
+(*conversion from sequence to list*)
+fun list_of xq =
+  (case pull xq of
+    None => []
+  | Some (x, xq') => x :: list_of xq');
+
+(*conversion from list to sequence*)
+fun of_list xs = foldr cons (xs, empty);
+
+
+(*map the function f over the sequence, making a new sequence*)
+fun map f xq =
+  make (fn () =>
+    (case pull xq of
+      None => None
+    | Some (x, xq') => Some (f x, map f xq')));
+
+(*map over a sequence xq, append the sequence yq*)
+fun mapp f xq yq =
+  let
+    fun copy s =
+      make (fn () =>
+        (case pull s of
+          None => pull yq
+        | Some (x, s') => Some (f x, copy s')))
+  in copy xq end;
+
+(*sequence append:  put the elements of xq in front of those of yq*)
+fun append (xq, yq) =
+  let
+    fun copy s =
+      make (fn () =>
+        (case pull s of
+          None => pull yq
+        | Some (x, s') => Some (x, copy s')))
+  in copy xq end;
+
+(*filter sequence by predicate*)
+fun filter pred xq =
+  let
+    fun copy s =
+      make (fn () =>
+        (case pull s of
+          None => None
+        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
+  in copy xq end;
+
+(*flatten a sequence of sequences to a single sequence*)
+fun flat xqq =
+  make (fn () =>
+    (case pull xqq of
+      None => None
+    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
+
+(*interleave elements of xq with those of yq -- fairer than append*)
+fun interleave (xq, yq) =
+  make (fn () =>
+    (case pull xq of
+      None => pull yq
+    | Some (x, xq') => Some (x, interleave (yq, xq'))));
+
+
+(*functional to print a sequence, up to "count" elements;
+  the function prelem should print the element number and also the element*)
+fun print prelem count seq =
+  let
+    fun pr (k, xq) =
+      if k > count then ()
+      else
+        (case pull xq of
+          None => ()
+        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
+  in pr (1, seq) end;
+
+(*accumulating a function over a sequence; this is lazy*)
+fun it_right f (xq, yq) =
+  let
+    fun its s =
+      make (fn () =>
+        (case pull s of
+          None => pull yq
+        | Some (a, s') => pull (f (a, its s'))))
+  in its xq end;
+
+
+end;
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/tactic.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -68,7 +68,7 @@
   val net_resolve_tac	: thm list -> int -> tactic
   val orderlist		: (int * 'a) list -> 'a list
   val PRIMITIVE		: (thm -> thm) -> tactic  
-  val PRIMSEQ		: (thm -> thm Sequence.seq) -> tactic  
+  val PRIMSEQ		: (thm -> thm Seq.seq) -> tactic  
   val prune_params_tac	: tactic
   val rename_tac	: string -> int -> tactic
   val rename_last_tac	: string -> string list -> int -> tactic
@@ -99,10 +99,10 @@
 
 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
 fun trace_goalno_tac tac i st =  
-    case Sequence.pull(tac i st) of
-	None    => Sequence.null
+    case Seq.pull(tac i st) of
+	None    => Seq.empty
       | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
-    			 Sequence.seqof(fn()=> seqcell));
+    			 Seq.make(fn()=> seqcell));
 
 
 (*Convert all Vars in a theorem to Frees.  Also return a function for 
@@ -137,15 +137,15 @@
     in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
         |> implies_intr_list (List.take(hyps, i-1) @ hyps')
         |> thaw
-        |> Sequence.single
+        |> Seq.single
     end
-    handle _ => Sequence.null;
+    handle _ => Seq.empty;
 
 
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic tac rl =
   let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
-  in case Sequence.pull (tac st)  of
+  in case Seq.pull (tac st)  of
 	None        => raise THM("rule_by_tactic", 0, [rl])
       | Some(st',_) => Thm.varifyT (thaw st')
   end;
@@ -153,10 +153,10 @@
 (*** Basic tactics ***)
 
 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
-fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
+fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
 
 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
-fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
+fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
 
 (*** The following fail if the goal number is out of range:
      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
@@ -221,7 +221,7 @@
 	val assumed = implies_elim_list frozth (map assume froz_prems)
 	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
 					assumed;
-    in  Sequence.single (thawfn implied)  end
+    in  Seq.single (thawfn implied)  end
 end; 
 
 
@@ -315,7 +315,7 @@
 	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
 			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
       val arg = (false, rl, nprems_of rl)
-      val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
+      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   in  th  end
   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
 
@@ -352,12 +352,12 @@
 
 (*Introduce the given proposition as a lemma and subgoal*)
 fun subgoal_tac sprop i st = 
-  let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
+  let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
       val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
   in  
       if null (term_tvars concl') then ()
       else warning"Type variables in new subgoal: add a type constraint?";
-      Sequence.single st'
+      Seq.single st'
   end;
 
 (*Introduce a list of lemmas and subgoals*)
@@ -496,7 +496,7 @@
 (*** Meta-Rewriting Tactics ***)
 
 fun result1 tacf mss thm =
-  apsome fst (Sequence.pull (tacf mss thm));
+  apsome fst (Seq.pull (tacf mss thm));
 
 val simple_prover =
   result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/tctical.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -13,7 +13,7 @@
 
 signature TACTICAL =
   sig
-  type tactic  (* = thm -> thm Sequence.seq*)
+  type tactic  (* = thm -> thm Seq.seq*)
   val all_tac           : tactic
   val ALLGOALS          : (int -> tactic) -> tactic   
   val APPEND            : tactic * tactic -> tactic
@@ -55,8 +55,8 @@
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
-  val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
-  val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
+  val traced_tac        : (thm -> (thm * thm Seq.seq) option) -> tactic
+  val tracify           : bool ref -> tactic -> thm -> thm Seq.seq
   val trace_REPEAT      : bool ref
   val TRY               : tactic -> tactic
   val TRYALL            : (int -> tactic) -> tactic   
@@ -72,45 +72,45 @@
     if length of sequence = 0 then the tactic does not apply;
     if length > 1 then backtracking on the alternatives can occur.*)
 
-type tactic = thm -> thm Sequence.seq;
+type tactic = thm -> thm Seq.seq;
 
 
 (*** LCF-style tacticals ***)
 
 (*the tactical THEN performs one tactic followed by another*)
-fun (tac1 THEN tac2) st = Sequence.flats (Sequence.maps tac2 (tac1 st));
+fun (tac1 THEN tac2) st = Seq.flat (Seq.map tac2 (tac1 st));
 
 
 (*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
   Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
   Does not backtrack to tac2 if tac1 was initially chosen. *)
 fun (tac1 ORELSE tac2) st =
-    case Sequence.pull(tac1 st) of
+    case Seq.pull(tac1 st) of
         None       => tac2 st
-      | sequencecell => Sequence.seqof(fn()=> sequencecell);
+      | sequencecell => Seq.make(fn()=> sequencecell);
 
 
 (*The tactical APPEND combines the results of two tactics.
   Like ORELSE, but allows backtracking on both tac1 and tac2.
   The tactic tac2 is not applied until needed.*)
 fun (tac1 APPEND tac2) st = 
-  Sequence.append(tac1 st,
-                  Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+  Seq.append(tac1 st,
+                  Seq.make(fn()=> Seq.pull (tac2 st)));
 
 (*Like APPEND, but interleaves results of tac1 and tac2.*)
 fun (tac1 INTLEAVE tac2) st = 
-    Sequence.interleave(tac1 st,
-                        Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+    Seq.interleave(tac1 st,
+                        Seq.make(fn()=> Seq.pull (tac2 st)));
 
 (*Conditional tactic.
         tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
         tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
 *)
 fun (tac THEN_ELSE (tac1, tac2)) st = 
-    case Sequence.pull(tac st) of
+    case Seq.pull(tac st) of
         None    => tac2 st              (*failed; try tactic 2*)
-      | seqcell => Sequence.flats       (*succeeded; use tactic 1*)
-                    (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
+      | seqcell => Seq.flat       (*succeeded; use tactic 1*)
+                    (Seq.map tac1 (Seq.make(fn()=> seqcell)));
 
 
 (*Versions for combining tactic-valued functions, as in
@@ -121,17 +121,17 @@
 fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
 
 (*passes all proofs through unchanged;  identity of THEN*)
-fun all_tac st = Sequence.single st;
+fun all_tac st = Seq.single st;
 
 (*passes no proofs through;  identity of ORELSE and APPEND*)
-fun no_tac st  = Sequence.null;
+fun no_tac st  = Seq.empty;
 
 
 (*Make a tactic deterministic by chopping the tail of the proof sequence*)
 fun DETERM tac st =  
-      case Sequence.pull (tac st) of
-              None => Sequence.null
-            | Some(x,_) => Sequence.cons(x, Sequence.null);
+      case Seq.pull (tac st) of
+              None => Seq.empty
+            | Some(x,_) => Seq.cons(x, Seq.empty);
 
 
 (*Conditional tactical: testfun controls which tactic to use next.
@@ -148,15 +148,15 @@
   (*This version of EVERY avoids backtracking over repeated states*)
 
   fun EVY (trail, []) st = 
-	Sequence.seqof (fn()=> Some(st, 
-			Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
+	Seq.make (fn()=> Some(st, 
+			Seq.make (fn()=> Seq.pull (evyBack trail))))
     | EVY (trail, tac::tacs) st = 
-	  case Sequence.pull(tac st) of
+	  case Seq.pull(tac st) of
 	      None    => evyBack trail              (*failed: backtrack*)
 	    | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
-  and evyBack [] = Sequence.null (*no alternatives*)
+  and evyBack [] = Seq.empty (*no alternatives*)
     | evyBack ((st',q,tacs)::trail) =
-	  case Sequence.pull q of
+	  case Seq.pull q of
 	      None        => evyBack trail
 	    | Some(st,q') => if eq_thm (st',st) 
 			     then evyBack ((st',q',tacs)::trail)
@@ -192,13 +192,13 @@
 (*Print the current proof state and pass it on.*)
 val print_tac = 
     (fn st => 
-     (print_goals (!goals_limit) st; Sequence.single st));
+     (print_goals (!goals_limit) st; Seq.single st));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =  
   (prs"** Press RETURN to continue: ";
-   if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st
-   else (prs"Goodbye\n";  Sequence.null));
+   if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
+   else (prs"Goodbye\n";  Seq.empty));
 
 exception TRACE_EXIT of thm
 and TRACE_QUIT;
@@ -211,7 +211,7 @@
 fun exec_trace_command flag (tac, st) = 
    case TextIO.inputLine(TextIO.stdIn) of
        "\n" => tac st
-     | "f\n" => Sequence.null
+     | "f\n" => Seq.empty
      | "o\n" => (flag:=false;  tac st)
      | "s\n" => (suppress_tracing:=true;  tac st)
      | "x\n" => (prs"Exiting now\n";  raise (TRACE_EXIT st))
@@ -237,8 +237,8 @@
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
 fun traced_tac seqf st = 
     (suppress_tracing := false;
-     Sequence.seqof (fn()=> seqf st
-                         handle TRACE_EXIT st' => Some(st', Sequence.null)));
+     Seq.make (fn()=> seqf st
+                         handle TRACE_EXIT st' => Some(st', Seq.empty)));
 
 
 (*Deterministic REPEAT: only retains the first outcome; 
@@ -246,10 +246,10 @@
   If non-negative, n bounds the number of repetitions.*)
 fun REPEAT_DETERM_N n tac = 
   let val tac = tracify trace_REPEAT tac
-      fun drep 0 st = Some(st, Sequence.null)
+      fun drep 0 st = Some(st, Seq.empty)
         | drep n st =
-           (case Sequence.pull(tac st) of
-                None       => Some(st, Sequence.null)
+           (case Seq.pull(tac st) of
+                None       => Some(st, Seq.empty)
               | Some(st',_) => drep (n-1) st')
   in  traced_tac (drep n)  end;
 
@@ -260,11 +260,11 @@
 fun REPEAT tac = 
   let val tac = tracify trace_REPEAT tac
       fun rep qs st = 
-        case Sequence.pull(tac st) of
-            None       => Some(st, Sequence.seqof(fn()=> repq qs))
+        case Seq.pull(tac st) of
+            None       => Some(st, Seq.make(fn()=> repq qs))
           | Some(st',q) => rep (q::qs) st'
       and repq [] = None
-        | repq(q::qs) = case Sequence.pull q of
+        | repq(q::qs) = case Seq.pull q of
             None       => repq qs
           | Some(st,q) => rep (q::qs) st
   in  traced_tac (rep [])  end;
@@ -277,12 +277,12 @@
 (** Filtering tacticals **)
 
 (*Returns all states satisfying the predicate*)
-fun FILTER pred tac st = Sequence.filters pred (tac st);
+fun FILTER pred tac st = Seq.filter pred (tac st);
 
 (*Returns all changed states*)
 fun CHANGED tac st = 
     let fun diff st' = not (eq_thm(st,st'))
-    in  Sequence.filters diff (tac st)  end;
+    in  Seq.filter diff (tac st)  end;
 
 
 (*** Tacticals based on subgoal numbering ***)
@@ -320,7 +320,7 @@
 
 (*Make a tactic for subgoal i, if there is one.  *)
 fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
-                             handle Subscript => Sequence.null;
+                             handle Subscript => Seq.empty;
 
 
 (*** SELECT_GOAL ***)
@@ -362,7 +362,7 @@
   let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
 	  eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
       fun next st = bicompose false (false, restore st, nprems_of st) i st0
-  in  Sequence.flats (Sequence.maps next (tac eq_cprem))
+  in  Seq.flat (Seq.map next (tac eq_cprem))
   end;
 
 (* (!!selct. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
@@ -373,12 +373,12 @@
 (* Prevent the subgoal's assumptions from becoming additional subgoals in the
    new proof state by enclosing them by a universal quantification *)
 fun protect_subgoal st i =
-        Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
+        Seq.hd (bicompose false (false,dummy_quant_rl,1) i st)
         handle _ => error"SELECT_GOAL -- impossible error???";
 
 fun SELECT_GOAL tac i st = 
   case (i, List.drop(prems_of st, i-1)) of
-      (_,[]) => Sequence.null
+      (_,[]) => Seq.empty
     | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
     | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
     | (_, _::_) => select tac st i;
@@ -489,7 +489,7 @@
       (*function to replace the current subgoal*)
       fun next st = bicompose false (false, relift st, nprems_of st)
                     i state
-  in  Sequence.flats (Sequence.maps next (tacf subprems st0))
+  in  Seq.flat (Seq.map next (tacf subprems st0))
   end;
 end;
 
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/thm.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -19,8 +19,7 @@
   (*certified terms*)
   type cterm
   exception CTERM of string
-  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ,
-                                    maxidx: int}
+  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
   val term_of           : cterm -> term
   val cterm_of          : Sign.sg -> term -> cterm
   val ctyp_of_term      : cterm -> ctyp
@@ -121,7 +120,7 @@
   val equal_intr        : thm -> thm -> thm
   val equal_elim        : thm -> thm -> thm
   val implies_intr_hyps : thm -> thm
-  val flexflex_rule     : thm -> thm Sequence.seq
+  val flexflex_rule     : thm -> thm Seq.seq
   val instantiate       :
     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
   val trivial           : cterm -> thm
@@ -131,14 +130,14 @@
   val dest_state        : thm * int ->
     (term * term) list * term list * term * term
   val lift_rule         : (thm * int) -> thm -> thm
-  val assumption        : int -> thm -> thm Sequence.seq
+  val assumption        : int -> thm -> thm Seq.seq
   val eq_assumption     : int -> thm -> thm
   val rotate_rule       : int -> int -> thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val bicompose         : bool -> bool * thm * int ->
-    int -> thm -> thm Sequence.seq
+    int -> thm -> thm Seq.seq
   val biresolution      : bool -> (bool * thm) list ->
-    int -> thm -> thm Sequence.seq
+    int -> thm -> thm Seq.seq
 
   (*meta simplification*)
   exception SIMPLIFIER of string * thm
@@ -1016,7 +1015,7 @@
                      prop = newprop})
           end;
       val (tpairs,_) = Logic.strip_flexpairs prop
-  in Sequence.maps newthm
+  in Seq.map newthm
             (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
   end;
 
@@ -1181,9 +1180,9 @@
                    Logic.rule_of (tpairs, Bs, C)
                else (*normalize the new rule fully*)
                    Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
-      fun addprfs [] = Sequence.null
-        | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
-             (Sequence.mapp newth
+      fun addprfs [] = Seq.empty
+        | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull
+             (Seq.mapp newth
                 (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
                 (addprfs apairs)))
   in  addprfs (Logic.assum_pairs Bi)  end;
@@ -1349,7 +1348,7 @@
   nsubgoal is the number of new subgoals (written m above).
   Curried so that resolution calls dest_state only once.
 *)
-local open Sequence; exception COMPOSE
+local exception COMPOSE
 in
 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
                         (eres_flg, orule, nsubgoal) =
@@ -1387,7 +1386,7 @@
                  shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
                  hyps = union_term(rhyps,shyps),
                  prop = Logic.rule_of normp}
-        in  cons(th, thq)  end  handle COMPOSE => thq
+        in  Seq.cons(th, thq)  end  handle COMPOSE => thq
      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
@@ -1403,23 +1402,23 @@
      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
      val dpairs = BBi :: (rtpairs@stpairs);
      (*elim-resolution: try each assumption in turn.  Initially n=1*)
-     fun tryasms (_, _, []) = null
+     fun tryasms (_, _, []) = Seq.empty
        | tryasms (As, n, (t,u)::apairs) =
-          (case pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
+          (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
                None                   => tryasms (As, n+1, apairs)
              | cell as Some((_,tpairs),_) =>
-                   its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
-                       (seqof (fn()=> cell),
-                        seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
+                   Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
+                       (Seq.make (fn()=> cell),
+                        Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs)))));
      fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
        | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
      (*ordinary resolution*)
-     fun res(None) = null
+     fun res(None) = Seq.empty
        | res(cell as Some((_,tpairs),_)) =
-             its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
-                       (seqof (fn()=> cell), null)
+             Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
+                       (Seq.make (fn()=> cell), Seq.empty)
  in  if eres_flg then eres(rev rAs)
-     else res(pull(Unify.unifiers(sign, env, dpairs)))
+     else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  end;
 end;  (*open Sequence*)
 
@@ -1444,14 +1443,14 @@
         val B = Logic.strip_assums_concl Bi;
         val Hs = Logic.strip_assums_hyp Bi;
         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
-        fun res [] = Sequence.null
+        fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
               if could_bires (Hs, B, eres_flg, rule)
-              then Sequence.seqof (*delay processing remainder till needed*)
+              then Seq.make (*delay processing remainder till needed*)
                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
                                res brules))
               else res brules
-    in  Sequence.flats (res brules)  end;
+    in  Seq.flat (res brules)  end;
 
 
 
diff -r a045600f0c98 -r 957c887b89b5 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/unify.ML	Fri Nov 21 15:27:43 1997 +0100
@@ -25,9 +25,9 @@
   val combound : (term*int*int) -> term
   val rlist_abs: (string*typ)list * term -> term   
   val smash_unifiers : Sign.sg * Envir.env * (term*term)list
-	-> (Envir.env Sequence.seq)
+	-> (Envir.env Seq.seq)
   val unifiers: Sign.sg * Envir.env * ((term*term)list)
-	-> (Envir.env * (term * term)list) Sequence.seq
+	-> (Envir.env * (term * term)list) Seq.seq
   end;
 
 structure Unify	: UNIFY = 
@@ -386,16 +386,16 @@
   The order for trying projections is crucial in ?b'(?a)   
   NB "vname" is only used in the call to make_args!!   *)
 fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
-	: (term * (Envir.env * dpair list))Sequence.seq =
+	: (term * (Envir.env * dpair list))Seq.seq =
 let (*Produce copies of uarg and cons them in front of uargs*)
     fun copycons uarg (uargs, (env, dpairs)) =
-	Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
+	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
 	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
 		 (env, dpairs)));
 	(*Produce sequence of all possible ways of copying the arg list*)
-    fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
+    fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
       | copyargs (uarg::uargs) =
-	    Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
+	    Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
     val (uhead,uargs) = strip_comb u;
     val base = body_type env (fastype env (rbinder,uhead));
     fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
@@ -404,7 +404,7 @@
     fun projenv (head, (Us,bary), targ, tail) = 
 	let val env = if !trace_types then test_unify_types(base,bary,env)
 		      else unify_types(base,bary,env)
-	in Sequence.seqof (fn () =>  
+	in Seq.make (fn () =>  
 	    let val (env',args) = make_args vname (Ts,env,Us);
 		(*higher-order projection: plug in targs for bound vars*)
 		fun plugin arg = list_comb(head_of arg, targs);
@@ -413,7 +413,7 @@
 		    (*may raise exception CANTUNIFY*)
 	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
 			tail)
-	    end  handle CANTUNIFY => Sequence.pull tail)
+	    end  handle CANTUNIFY => Seq.pull tail)
 	end handle CANTUNIFY => tail;
     (*make a list of projections*)
     fun make_projs (T::Ts, targ::targs) =
@@ -425,12 +425,12 @@
 	       (projenv(bvar, strip_type env T, targ, matchfun projs))
       | matchfun [] = (*imitation last of all*)
 	      (case uhead of
-		 Const _ => Sequence.maps joinargs (copyargs uargs)
-	       | Free _  => Sequence.maps joinargs (copyargs uargs)
-	       | _ => Sequence.null)  (*if Var, would be a loop!*)
+		 Const _ => Seq.map joinargs (copyargs uargs)
+	       | Free _  => Seq.map joinargs (copyargs uargs)
+	       | _ => Seq.empty)  (*if Var, would be a loop!*)
 in case uhead of
 	Abs(a, T, body) =>
-	    Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
+	    Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 
 		(mc ((a,T)::rbinder,
 			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
       | Var (w,uary) => 
@@ -438,7 +438,7 @@
 	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
 		val tabs = combound(newhd, 0, length Ts)
 		val tsub = list_comb(newhd,targs)
-	    in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
+	    in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
 	    end
       | _ =>  matchfun(rev(make_projs(Ts, targs)))
 end
@@ -447,7 +447,7 @@
 
 (*Call matchcopy to produce assignments to the variable in the dpair*)
 fun MATCH (env, (rbinder,t,u), dpairs)
-	: (Envir.env * dpair list)Sequence.seq = 
+	: (Envir.env * dpair list)Seq.seq = 
   let val (Var(v,T), targs) = strip_comb t;
       val Ts = binder_types env T;
       fun new_dset (u', (env',dpairs')) =
@@ -455,7 +455,7 @@
 	  case Envir.lookup(env',v) of
 	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
 	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
-  in Sequence.maps new_dset
+  in Seq.map new_dset
          (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   end;
 
@@ -620,9 +620,9 @@
   Returns flex-flex disagreement pairs NOT IN normal form. 
   SIMPL may raise exception CANTUNIFY. *)
 fun hounifiers (sg,env, tus : (term*term)list) 
-  : (Envir.env * (term*term)list)Sequence.seq =
+  : (Envir.env * (term*term)list)Seq.seq =
   let fun add_unify tdepth ((env,dpairs), reseq) =
-	  Sequence.seqof (fn()=>
+	  Seq.make (fn()=>
 	  let val (env',flexflex,flexrigid) = 
 	       (if tdepth> !trace_bound andalso !trace_simp
 		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
@@ -631,25 +631,25 @@
 	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
 	    | dp::frigid' => 
 		if tdepth > !search_bound then
-		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
+		    (prs"***Unification bound exceeded\n"; Seq.pull reseq)
 		else
 		(if tdepth > !trace_bound then
 		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
 		 else ();
-		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
+		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
 			   (MATCH (env',dp, frigid'@flexflex), reseq)))
 	  end
 	  handle CANTUNIFY => 
 	    (if tdepth > !trace_bound then writeln"Failure node" else ();
-	     Sequence.pull reseq));
+	     Seq.pull reseq));
      val dps = map (fn(t,u)=> ([],t,u)) tus
   in sgr := sg;
-     add_unify 1 ((env,dps), Sequence.null) 
+     add_unify 1 ((env,dps), Seq.empty) 
   end;
 
 fun unifiers(params) =
-      Sequence.cons((Pattern.unify(params), []),   Sequence.null)
-      handle Pattern.Unif => Sequence.null
+      Seq.cons((Pattern.unify(params), []),   Seq.empty)
+      handle Pattern.Unif => Seq.empty
            | Pattern.Pattern => hounifiers(params);
 
 
@@ -682,7 +682,7 @@
   foldr smash_flexflex1 (tpairs, env);
 
 (*Returns unifiers with no remaining disagreement pairs*)
-fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
-    Sequence.maps smash_flexflex (unifiers(sg,env,tus));
+fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
+    Seq.map smash_flexflex (unifiers(sg,env,tus));
 
 end;