changed Sequence interface (now Seq, in seq.ML);
authorwenzelm
Fri Nov 21 15:27:43 1997 +0100 (1997-11-21)
changeset 4270957c887b89b5
parent 4269 a045600f0c98
child 4271 3a82492e70c5
changed Sequence interface (now Seq, in seq.ML);
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/search.ML
src/Pure/seq.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/thm.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Nov 21 15:26:22 1997 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Fri Nov 21 15:27:43 1997 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  	Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \
     1.5  	axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
     1.6  	goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
     1.7 -	pattern.ML pure_thy.ML search.ML section_utils.ML sequence.ML sign.ML \
     1.8 +	pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \
     1.9  	sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
    1.10  	type.ML type_infer.ML unify.ML
    1.11  
     2.1 --- a/src/Pure/ROOT.ML	Fri Nov 21 15:26:22 1997 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Fri Nov 21 15:27:43 1997 +0100
     2.3 @@ -27,7 +27,7 @@
     2.4  use "type_infer.ML";
     2.5  use "type.ML";
     2.6  use "sign.ML";
     2.7 -use "sequence.ML";
     2.8 +use "seq.ML";
     2.9  use "envir.ML";
    2.10  use "pattern.ML";
    2.11  use "unify.ML";
     3.1 --- a/src/Pure/display.ML	Fri Nov 21 15:26:22 1997 +0100
     3.2 +++ b/src/Pure/display.ML	Fri Nov 21 15:27:43 1997 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4    val print_data	: theory -> string -> unit
     3.5    val print_thm		: thm -> unit
     3.6    val prth		: thm -> thm
     3.7 -  val prthq		: thm Sequence.seq -> thm Sequence.seq
     3.8 +  val prthq		: thm Seq.seq -> thm Seq.seq
     3.9    val prths		: thm list -> thm list
    3.10    val show_hyps		: bool ref
    3.11    val string_of_cterm	: cterm -> string
    3.12 @@ -67,7 +67,7 @@
    3.13  
    3.14  (*Print and return a sequence of theorems, separated by blank lines. *)
    3.15  fun prthq thseq =
    3.16 -  (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
    3.17 +  (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
    3.18  
    3.19  (*Print and return a list of theorems, separated by blank lines. *)
    3.20  fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths);
     4.1 --- a/src/Pure/drule.ML	Fri Nov 21 15:26:22 1997 +0100
     4.2 +++ b/src/Pure/drule.ML	Fri Nov 21 15:27:43 1997 +0100
     4.3 @@ -256,7 +256,7 @@
     4.4  
     4.5  (*Resolution: exactly one resolvent must be produced.*)
     4.6  fun tha RSN (i,thb) =
     4.7 -  case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
     4.8 +  case Seq.chop (2, biresolution false [(false,tha)] i thb) of
     4.9        ([th],_) => th
    4.10      | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
    4.11      |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
    4.12 @@ -267,7 +267,7 @@
    4.13  (*For joining lists of rules*)
    4.14  fun thas RLN (i,thbs) =
    4.15    let val resolve = biresolution false (map (pair false) thas) i
    4.16 -      fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
    4.17 +      fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
    4.18    in  List.concat (map resb thbs)  end;
    4.19  
    4.20  fun thas RL thbs = thas RLN (1,thbs);
    4.21 @@ -289,7 +289,7 @@
    4.22    with no lifting or renaming!  Q may contain ==> or meta-quants
    4.23    ALWAYS deletes premise i *)
    4.24  fun compose(tha,i,thb) =
    4.25 -    Sequence.list_of_s (bicompose false (false,tha,0) i thb);
    4.26 +    Seq.list_of (bicompose false (false,tha,0) i thb);
    4.27  
    4.28  (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
    4.29  fun tha COMP thb =
     5.1 --- a/src/Pure/goals.ML	Fri Nov 21 15:26:22 1997 +0100
     5.2 +++ b/src/Pure/goals.ML	Fri Nov 21 15:27:43 1997 +0100
     5.3 @@ -76,7 +76,7 @@
     5.4  
     5.5  (*Each level of goal stack includes a proof state and alternative states,
     5.6    the output of the tactic applied to the preceeding level.  *)
     5.7 -type gstack = (thm * thm Sequence.seq) list;
     5.8 +type gstack = (thm * thm Seq.seq) list;
     5.9  
    5.10  datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
    5.11  
    5.12 @@ -101,7 +101,7 @@
    5.13  
    5.14  (*List of previous goal stacks, for the undo operation.  Set by setstate. 
    5.15    A list of lists!*)
    5.16 -val undo_list = ref([[(dummy, Sequence.null)]] : gstack list);
    5.17 +val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
    5.18  
    5.19  (* Stack of proof attempts *)
    5.20  val proofstack = ref([]: proof list);
    5.21 @@ -137,7 +137,7 @@
    5.22        (*discharges assumptions from state in the order they appear in goal;
    5.23  	checks (if requested) that resulting theorem is equivalent to goal. *)
    5.24        fun mkresult (check,state) =
    5.25 -        let val state = Sequence.hd (flexflex_rule state)
    5.26 +        let val state = Seq.hd (flexflex_rule state)
    5.27  	    		handle THM _ => state   (*smash flexflex pairs*)
    5.28  	    val ngoals = nprems_of state
    5.29              val th = strip_shyps (implies_intr_list cAs state)
    5.30 @@ -199,7 +199,7 @@
    5.31    let val (prems, st0, mkresult) = prepare_proof rths chorn
    5.32        val tac = EVERY (tacsf prems)
    5.33        fun statef() = 
    5.34 -	  (case Sequence.pull (tac st0) of 
    5.35 +	  (case Seq.pull (tac st0) of 
    5.36  	       Some(st,_) => st
    5.37  	     | _ => error ("prove_goal: tactic failed"))
    5.38    in  mkresult (true, cond_timeit (!proof_timing) statef)  end
    5.39 @@ -243,7 +243,7 @@
    5.40    !print_current_goals_fn (length pairs) (!goals_limit) th;
    5.41  
    5.42  (*Printing can raise exceptions, so the assignment occurs last.
    5.43 -  Can do   setstate[(st,Sequence.null)]  to set st as the state.  *)
    5.44 +  Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
    5.45  fun setstate newgoals = 
    5.46    (print_top (pop newgoals);  undo_list := newgoals :: !undo_list);
    5.47  
    5.48 @@ -307,7 +307,7 @@
    5.49  fun goalw_cterm rths chorn = 
    5.50    let val (prems, st0, mkresult) = prepare_proof rths chorn
    5.51    in  undo_list := [];
    5.52 -      setstate [ (st0, Sequence.null) ];  
    5.53 +      setstate [ (st0, Seq.empty) ];  
    5.54        curr_prems := prems;
    5.55        curr_mkresult := mkresult;
    5.56        prems
    5.57 @@ -324,7 +324,7 @@
    5.58  
    5.59  (*Proof step "by" the given tactic -- apply tactic to the proof state*)
    5.60  fun by_com tac ((th,ths), pairs) : gstack =
    5.61 -  (case  Sequence.pull(tac th)  of
    5.62 +  (case  Seq.pull(tac th)  of
    5.63       None      => error"by: tactic failed"
    5.64     | Some(th2,ths2) => 
    5.65         (if eq_thm(th,th2) 
    5.66 @@ -346,7 +346,7 @@
    5.67    If none at this level, try earlier levels*)
    5.68  fun backtrack [] = error"back: no alternatives"
    5.69    | backtrack ((th,thstr) :: pairs) =
    5.70 -     (case Sequence.pull thstr of
    5.71 +     (case Seq.pull thstr of
    5.72  	  None      => (writeln"Going back a level..."; backtrack pairs)
    5.73  	| Some(th2,thstr2) =>  
    5.74  	   (if eq_thm(th,th2) 
     6.1 --- a/src/Pure/search.ML	Fri Nov 21 15:26:22 1997 +0100
     6.2 +++ b/src/Pure/search.ML	Fri Nov 21 15:27:43 1997 +0100
     6.3 @@ -47,14 +47,14 @@
     6.4   let val tac = tracify trace_DEPTH_FIRST tac
     6.5       fun depth used [] = None
     6.6         | depth used (q::qs) =
     6.7 -	  case Sequence.pull q of
     6.8 +	  case Seq.pull q of
     6.9  	      None         => depth used qs
    6.10  	    | Some(st,stq) => 
    6.11  		if satp st andalso not (gen_mem eq_thm (st, used))
    6.12 -		then Some(st, Sequence.seqof
    6.13 +		then Some(st, Seq.make
    6.14  			         (fn()=> depth (st::used) (stq::qs)))
    6.15  		else depth used (tac st :: stq :: qs)
    6.16 -  in  traced_tac (fn st => depth [] ([Sequence.single st]))  end;
    6.17 +  in  traced_tac (fn st => depth [] ([Seq.single st]))  end;
    6.18  
    6.19  
    6.20  
    6.21 @@ -136,11 +136,11 @@
    6.22  		    writeln (string_of_int np ^ 
    6.23  			     implode (map (fn _ => "*") qs))
    6.24  		else ();
    6.25 -		Sequence.pull q) of
    6.26 +		Seq.pull q) of
    6.27  	     None         => depth (bnd,inc) qs
    6.28  	   | Some(st,stq) => 
    6.29  	       if satp st	(*solution!*)
    6.30 -	       then Some(st, Sequence.seqof
    6.31 +	       then Some(st, Seq.make
    6.32  			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
    6.33  
    6.34  	       else 
    6.35 @@ -185,7 +185,7 @@
    6.36  
    6.37  (*For creating output sequence*)
    6.38  fun some_of_list []     = None
    6.39 -  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
    6.40 +  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
    6.41  
    6.42  
    6.43  (*Best-first search for a state that satisfies satp (incl initial state)
    6.44 @@ -205,8 +205,8 @@
    6.45  	       then writeln("state size = " ^ string_of_int n ^ 
    6.46  		         "  queue length =" ^ string_of_int (length nprfs))  
    6.47                 else ();
    6.48 -	     bfs (Sequence.list_of_s (tac prf), nprfs))
    6.49 -      fun btac st = bfs (Sequence.list_of_s (tac0 st),  [])
    6.50 +	     bfs (Seq.list_of (tac prf), nprfs))
    6.51 +      fun btac st = bfs (Seq.list_of (tac0 st),  [])
    6.52    in traced_tac btac end;
    6.53  
    6.54  (*Ordinary best-first search, with no initial tactic*)
    6.55 @@ -215,7 +215,7 @@
    6.56  (*Breadth-first search to satisfy satpred (including initial state) 
    6.57    SLOW -- SHOULD NOT USE APPEND!*)
    6.58  fun BREADTH_FIRST satpred tac = 
    6.59 -  let val tacf = Sequence.list_of_s o tac;
    6.60 +  let val tacf = Seq.list_of o tac;
    6.61        fun bfs prfs =
    6.62  	 (case  partition satpred prfs  of
    6.63  	      ([],[]) => []
    6.64 @@ -223,7 +223,7 @@
    6.65  		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
    6.66  		   bfs (List.concat (map tacf nonsats)))
    6.67  	    | (sats,_)  => sats)
    6.68 -  in (fn st => Sequence.s_of_list (bfs [st])) end;
    6.69 +  in (fn st => Seq.of_list (bfs [st])) end;
    6.70  
    6.71  
    6.72  (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
    6.73 @@ -242,7 +242,7 @@
    6.74  
    6.75  (*For creating output sequence*)
    6.76  fun some_of_list []     = None
    6.77 -  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
    6.78 +  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
    6.79  
    6.80  val trace_ASTAR = ref false; 
    6.81  
    6.82 @@ -262,8 +262,8 @@
    6.83  			 "  cost = " ^ string_of_int n ^ 
    6.84                           "  queue length =" ^ string_of_int (length nprfs))  
    6.85                 else ();
    6.86 -             bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
    6.87 -      fun tf st = bfs (Sequence.list_of_s (tac0 st), [], 0)
    6.88 +             bfs (Seq.list_of (tf prf), nprfs,level+1))
    6.89 +      fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
    6.90    in traced_tac tf end;
    6.91  
    6.92  (*Ordinary ASTAR, with no initial tactic*)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/seq.ML	Fri Nov 21 15:27:43 1997 +0100
     7.3 @@ -0,0 +1,155 @@
     7.4 +(*  Title:      Pure/seq.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +
     7.8 +Unbounded sequences implemented by closures.  RECOMPUTES if sequence
     7.9 +is re-inspected.  Memoing, using polymorphic refs, was found to be
    7.10 +slower!  (More GCs)
    7.11 +*)
    7.12 +
    7.13 +signature SEQ =
    7.14 +sig
    7.15 +  type 'a seq
    7.16 +  val make: (unit -> ('a * 'a seq) option) -> 'a seq
    7.17 +  val pull: 'a seq -> ('a * 'a seq) option
    7.18 +  val empty: 'a seq
    7.19 +  val cons: 'a * 'a seq -> 'a seq
    7.20 +  val single: 'a -> 'a seq
    7.21 +  val hd: 'a seq -> 'a
    7.22 +  val tl: 'a seq -> 'a seq
    7.23 +  val chop: int * 'a seq -> 'a list * 'a seq
    7.24 +  val list_of: 'a seq -> 'a list
    7.25 +  val of_list: 'a list -> 'a seq
    7.26 +  val map: ('a -> 'b) -> 'a seq -> 'b seq
    7.27 +  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    7.28 +  val append: 'a seq * 'a seq -> 'a seq
    7.29 +  val filter: ('a -> bool) -> 'a seq -> 'a seq
    7.30 +  val flat: 'a seq seq -> 'a seq
    7.31 +  val interleave: 'a seq * 'a seq -> 'a seq
    7.32 +  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    7.33 +  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    7.34 +end;
    7.35 +
    7.36 +structure Seq: SEQ =
    7.37 +struct
    7.38 +
    7.39 +
    7.40 +datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
    7.41 +
    7.42 +(*the abstraction for making a sequence*)
    7.43 +val make = Seq;
    7.44 +
    7.45 +(*return next sequence element as None or Some (x, xq)*)
    7.46 +fun pull (Seq f) = f ();
    7.47 +
    7.48 +
    7.49 +(*the empty sequence*)
    7.50 +val empty = make (fn () => None);
    7.51 +
    7.52 +(*prefix an element to the sequence -- use cons (x, xq) only if
    7.53 +  evaluation of xq need not be delayed, otherwise use
    7.54 +  make (fn () => Some (x, xq))*)
    7.55 +fun cons x_xq = make (fn () => Some x_xq);
    7.56 +
    7.57 +fun single x = cons (x, empty);
    7.58 +
    7.59 +(*head and tail -- beware of calling the sequence function twice!!*)
    7.60 +fun hd xq = #1 (the (pull xq))
    7.61 +and tl xq = #2 (the (pull xq));
    7.62 +
    7.63 +
    7.64 +(*the list of the first n elements, paired with rest of sequence;
    7.65 +  if length of list is less than n, then sequence had less than n elements*)
    7.66 +fun chop (n, xq) =
    7.67 +  if n <= 0 then ([], xq)
    7.68 +  else
    7.69 +    (case pull xq of
    7.70 +      None => ([], xq)
    7.71 +    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    7.72 +
    7.73 +(*conversion from sequence to list*)
    7.74 +fun list_of xq =
    7.75 +  (case pull xq of
    7.76 +    None => []
    7.77 +  | Some (x, xq') => x :: list_of xq');
    7.78 +
    7.79 +(*conversion from list to sequence*)
    7.80 +fun of_list xs = foldr cons (xs, empty);
    7.81 +
    7.82 +
    7.83 +(*map the function f over the sequence, making a new sequence*)
    7.84 +fun map f xq =
    7.85 +  make (fn () =>
    7.86 +    (case pull xq of
    7.87 +      None => None
    7.88 +    | Some (x, xq') => Some (f x, map f xq')));
    7.89 +
    7.90 +(*map over a sequence xq, append the sequence yq*)
    7.91 +fun mapp f xq yq =
    7.92 +  let
    7.93 +    fun copy s =
    7.94 +      make (fn () =>
    7.95 +        (case pull s of
    7.96 +          None => pull yq
    7.97 +        | Some (x, s') => Some (f x, copy s')))
    7.98 +  in copy xq end;
    7.99 +
   7.100 +(*sequence append:  put the elements of xq in front of those of yq*)
   7.101 +fun append (xq, yq) =
   7.102 +  let
   7.103 +    fun copy s =
   7.104 +      make (fn () =>
   7.105 +        (case pull s of
   7.106 +          None => pull yq
   7.107 +        | Some (x, s') => Some (x, copy s')))
   7.108 +  in copy xq end;
   7.109 +
   7.110 +(*filter sequence by predicate*)
   7.111 +fun filter pred xq =
   7.112 +  let
   7.113 +    fun copy s =
   7.114 +      make (fn () =>
   7.115 +        (case pull s of
   7.116 +          None => None
   7.117 +        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
   7.118 +  in copy xq end;
   7.119 +
   7.120 +(*flatten a sequence of sequences to a single sequence*)
   7.121 +fun flat xqq =
   7.122 +  make (fn () =>
   7.123 +    (case pull xqq of
   7.124 +      None => None
   7.125 +    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
   7.126 +
   7.127 +(*interleave elements of xq with those of yq -- fairer than append*)
   7.128 +fun interleave (xq, yq) =
   7.129 +  make (fn () =>
   7.130 +    (case pull xq of
   7.131 +      None => pull yq
   7.132 +    | Some (x, xq') => Some (x, interleave (yq, xq'))));
   7.133 +
   7.134 +
   7.135 +(*functional to print a sequence, up to "count" elements;
   7.136 +  the function prelem should print the element number and also the element*)
   7.137 +fun print prelem count seq =
   7.138 +  let
   7.139 +    fun pr (k, xq) =
   7.140 +      if k > count then ()
   7.141 +      else
   7.142 +        (case pull xq of
   7.143 +          None => ()
   7.144 +        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   7.145 +  in pr (1, seq) end;
   7.146 +
   7.147 +(*accumulating a function over a sequence; this is lazy*)
   7.148 +fun it_right f (xq, yq) =
   7.149 +  let
   7.150 +    fun its s =
   7.151 +      make (fn () =>
   7.152 +        (case pull s of
   7.153 +          None => pull yq
   7.154 +        | Some (a, s') => pull (f (a, its s'))))
   7.155 +  in its xq end;
   7.156 +
   7.157 +
   7.158 +end;
     8.1 --- a/src/Pure/tactic.ML	Fri Nov 21 15:26:22 1997 +0100
     8.2 +++ b/src/Pure/tactic.ML	Fri Nov 21 15:27:43 1997 +0100
     8.3 @@ -68,7 +68,7 @@
     8.4    val net_resolve_tac	: thm list -> int -> tactic
     8.5    val orderlist		: (int * 'a) list -> 'a list
     8.6    val PRIMITIVE		: (thm -> thm) -> tactic  
     8.7 -  val PRIMSEQ		: (thm -> thm Sequence.seq) -> tactic  
     8.8 +  val PRIMSEQ		: (thm -> thm Seq.seq) -> tactic  
     8.9    val prune_params_tac	: tactic
    8.10    val rename_tac	: string -> int -> tactic
    8.11    val rename_last_tac	: string -> string list -> int -> tactic
    8.12 @@ -99,10 +99,10 @@
    8.13  
    8.14  (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    8.15  fun trace_goalno_tac tac i st =  
    8.16 -    case Sequence.pull(tac i st) of
    8.17 -	None    => Sequence.null
    8.18 +    case Seq.pull(tac i st) of
    8.19 +	None    => Seq.empty
    8.20        | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
    8.21 -    			 Sequence.seqof(fn()=> seqcell));
    8.22 +    			 Seq.make(fn()=> seqcell));
    8.23  
    8.24  
    8.25  (*Convert all Vars in a theorem to Frees.  Also return a function for 
    8.26 @@ -137,15 +137,15 @@
    8.27      in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
    8.28          |> implies_intr_list (List.take(hyps, i-1) @ hyps')
    8.29          |> thaw
    8.30 -        |> Sequence.single
    8.31 +        |> Seq.single
    8.32      end
    8.33 -    handle _ => Sequence.null;
    8.34 +    handle _ => Seq.empty;
    8.35  
    8.36  
    8.37  (*Makes a rule by applying a tactic to an existing rule*)
    8.38  fun rule_by_tactic tac rl =
    8.39    let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
    8.40 -  in case Sequence.pull (tac st)  of
    8.41 +  in case Seq.pull (tac st)  of
    8.42  	None        => raise THM("rule_by_tactic", 0, [rl])
    8.43        | Some(st',_) => Thm.varifyT (thaw st')
    8.44    end;
    8.45 @@ -153,10 +153,10 @@
    8.46  (*** Basic tactics ***)
    8.47  
    8.48  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    8.49 -fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
    8.50 +fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
    8.51  
    8.52  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
    8.53 -fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
    8.54 +fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
    8.55  
    8.56  (*** The following fail if the goal number is out of range:
    8.57       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
    8.58 @@ -221,7 +221,7 @@
    8.59  	val assumed = implies_elim_list frozth (map assume froz_prems)
    8.60  	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
    8.61  					assumed;
    8.62 -    in  Sequence.single (thawfn implied)  end
    8.63 +    in  Seq.single (thawfn implied)  end
    8.64  end; 
    8.65  
    8.66  
    8.67 @@ -315,7 +315,7 @@
    8.68  	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    8.69  			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    8.70        val arg = (false, rl, nprems_of rl)
    8.71 -      val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
    8.72 +      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
    8.73    in  th  end
    8.74    handle Bind => raise THM("make_elim_preserve", 1, [rl]);
    8.75  
    8.76 @@ -352,12 +352,12 @@
    8.77  
    8.78  (*Introduce the given proposition as a lemma and subgoal*)
    8.79  fun subgoal_tac sprop i st = 
    8.80 -  let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
    8.81 +  let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
    8.82        val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
    8.83    in  
    8.84        if null (term_tvars concl') then ()
    8.85        else warning"Type variables in new subgoal: add a type constraint?";
    8.86 -      Sequence.single st'
    8.87 +      Seq.single st'
    8.88    end;
    8.89  
    8.90  (*Introduce a list of lemmas and subgoals*)
    8.91 @@ -496,7 +496,7 @@
    8.92  (*** Meta-Rewriting Tactics ***)
    8.93  
    8.94  fun result1 tacf mss thm =
    8.95 -  apsome fst (Sequence.pull (tacf mss thm));
    8.96 +  apsome fst (Seq.pull (tacf mss thm));
    8.97  
    8.98  val simple_prover =
    8.99    result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
     9.1 --- a/src/Pure/tctical.ML	Fri Nov 21 15:26:22 1997 +0100
     9.2 +++ b/src/Pure/tctical.ML	Fri Nov 21 15:27:43 1997 +0100
     9.3 @@ -13,7 +13,7 @@
     9.4  
     9.5  signature TACTICAL =
     9.6    sig
     9.7 -  type tactic  (* = thm -> thm Sequence.seq*)
     9.8 +  type tactic  (* = thm -> thm Seq.seq*)
     9.9    val all_tac           : tactic
    9.10    val ALLGOALS          : (int -> tactic) -> tactic   
    9.11    val APPEND            : tactic * tactic -> tactic
    9.12 @@ -55,8 +55,8 @@
    9.13    val THEN              : tactic * tactic -> tactic
    9.14    val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    9.15    val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
    9.16 -  val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
    9.17 -  val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
    9.18 +  val traced_tac        : (thm -> (thm * thm Seq.seq) option) -> tactic
    9.19 +  val tracify           : bool ref -> tactic -> thm -> thm Seq.seq
    9.20    val trace_REPEAT      : bool ref
    9.21    val TRY               : tactic -> tactic
    9.22    val TRYALL            : (int -> tactic) -> tactic   
    9.23 @@ -72,45 +72,45 @@
    9.24      if length of sequence = 0 then the tactic does not apply;
    9.25      if length > 1 then backtracking on the alternatives can occur.*)
    9.26  
    9.27 -type tactic = thm -> thm Sequence.seq;
    9.28 +type tactic = thm -> thm Seq.seq;
    9.29  
    9.30  
    9.31  (*** LCF-style tacticals ***)
    9.32  
    9.33  (*the tactical THEN performs one tactic followed by another*)
    9.34 -fun (tac1 THEN tac2) st = Sequence.flats (Sequence.maps tac2 (tac1 st));
    9.35 +fun (tac1 THEN tac2) st = Seq.flat (Seq.map tac2 (tac1 st));
    9.36  
    9.37  
    9.38  (*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
    9.39    Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
    9.40    Does not backtrack to tac2 if tac1 was initially chosen. *)
    9.41  fun (tac1 ORELSE tac2) st =
    9.42 -    case Sequence.pull(tac1 st) of
    9.43 +    case Seq.pull(tac1 st) of
    9.44          None       => tac2 st
    9.45 -      | sequencecell => Sequence.seqof(fn()=> sequencecell);
    9.46 +      | sequencecell => Seq.make(fn()=> sequencecell);
    9.47  
    9.48  
    9.49  (*The tactical APPEND combines the results of two tactics.
    9.50    Like ORELSE, but allows backtracking on both tac1 and tac2.
    9.51    The tactic tac2 is not applied until needed.*)
    9.52  fun (tac1 APPEND tac2) st = 
    9.53 -  Sequence.append(tac1 st,
    9.54 -                  Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
    9.55 +  Seq.append(tac1 st,
    9.56 +                  Seq.make(fn()=> Seq.pull (tac2 st)));
    9.57  
    9.58  (*Like APPEND, but interleaves results of tac1 and tac2.*)
    9.59  fun (tac1 INTLEAVE tac2) st = 
    9.60 -    Sequence.interleave(tac1 st,
    9.61 -                        Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
    9.62 +    Seq.interleave(tac1 st,
    9.63 +                        Seq.make(fn()=> Seq.pull (tac2 st)));
    9.64  
    9.65  (*Conditional tactic.
    9.66          tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
    9.67          tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
    9.68  *)
    9.69  fun (tac THEN_ELSE (tac1, tac2)) st = 
    9.70 -    case Sequence.pull(tac st) of
    9.71 +    case Seq.pull(tac st) of
    9.72          None    => tac2 st              (*failed; try tactic 2*)
    9.73 -      | seqcell => Sequence.flats       (*succeeded; use tactic 1*)
    9.74 -                    (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
    9.75 +      | seqcell => Seq.flat       (*succeeded; use tactic 1*)
    9.76 +                    (Seq.map tac1 (Seq.make(fn()=> seqcell)));
    9.77  
    9.78  
    9.79  (*Versions for combining tactic-valued functions, as in
    9.80 @@ -121,17 +121,17 @@
    9.81  fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
    9.82  
    9.83  (*passes all proofs through unchanged;  identity of THEN*)
    9.84 -fun all_tac st = Sequence.single st;
    9.85 +fun all_tac st = Seq.single st;
    9.86  
    9.87  (*passes no proofs through;  identity of ORELSE and APPEND*)
    9.88 -fun no_tac st  = Sequence.null;
    9.89 +fun no_tac st  = Seq.empty;
    9.90  
    9.91  
    9.92  (*Make a tactic deterministic by chopping the tail of the proof sequence*)
    9.93  fun DETERM tac st =  
    9.94 -      case Sequence.pull (tac st) of
    9.95 -              None => Sequence.null
    9.96 -            | Some(x,_) => Sequence.cons(x, Sequence.null);
    9.97 +      case Seq.pull (tac st) of
    9.98 +              None => Seq.empty
    9.99 +            | Some(x,_) => Seq.cons(x, Seq.empty);
   9.100  
   9.101  
   9.102  (*Conditional tactical: testfun controls which tactic to use next.
   9.103 @@ -148,15 +148,15 @@
   9.104    (*This version of EVERY avoids backtracking over repeated states*)
   9.105  
   9.106    fun EVY (trail, []) st = 
   9.107 -	Sequence.seqof (fn()=> Some(st, 
   9.108 -			Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
   9.109 +	Seq.make (fn()=> Some(st, 
   9.110 +			Seq.make (fn()=> Seq.pull (evyBack trail))))
   9.111      | EVY (trail, tac::tacs) st = 
   9.112 -	  case Sequence.pull(tac st) of
   9.113 +	  case Seq.pull(tac st) of
   9.114  	      None    => evyBack trail              (*failed: backtrack*)
   9.115  	    | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
   9.116 -  and evyBack [] = Sequence.null (*no alternatives*)
   9.117 +  and evyBack [] = Seq.empty (*no alternatives*)
   9.118      | evyBack ((st',q,tacs)::trail) =
   9.119 -	  case Sequence.pull q of
   9.120 +	  case Seq.pull q of
   9.121  	      None        => evyBack trail
   9.122  	    | Some(st,q') => if eq_thm (st',st) 
   9.123  			     then evyBack ((st',q',tacs)::trail)
   9.124 @@ -192,13 +192,13 @@
   9.125  (*Print the current proof state and pass it on.*)
   9.126  val print_tac = 
   9.127      (fn st => 
   9.128 -     (print_goals (!goals_limit) st; Sequence.single st));
   9.129 +     (print_goals (!goals_limit) st; Seq.single st));
   9.130  
   9.131  (*Pause until a line is typed -- if non-empty then fail. *)
   9.132  fun pause_tac st =  
   9.133    (prs"** Press RETURN to continue: ";
   9.134 -   if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st
   9.135 -   else (prs"Goodbye\n";  Sequence.null));
   9.136 +   if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
   9.137 +   else (prs"Goodbye\n";  Seq.empty));
   9.138  
   9.139  exception TRACE_EXIT of thm
   9.140  and TRACE_QUIT;
   9.141 @@ -211,7 +211,7 @@
   9.142  fun exec_trace_command flag (tac, st) = 
   9.143     case TextIO.inputLine(TextIO.stdIn) of
   9.144         "\n" => tac st
   9.145 -     | "f\n" => Sequence.null
   9.146 +     | "f\n" => Seq.empty
   9.147       | "o\n" => (flag:=false;  tac st)
   9.148       | "s\n" => (suppress_tracing:=true;  tac st)
   9.149       | "x\n" => (prs"Exiting now\n";  raise (TRACE_EXIT st))
   9.150 @@ -237,8 +237,8 @@
   9.151  (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
   9.152  fun traced_tac seqf st = 
   9.153      (suppress_tracing := false;
   9.154 -     Sequence.seqof (fn()=> seqf st
   9.155 -                         handle TRACE_EXIT st' => Some(st', Sequence.null)));
   9.156 +     Seq.make (fn()=> seqf st
   9.157 +                         handle TRACE_EXIT st' => Some(st', Seq.empty)));
   9.158  
   9.159  
   9.160  (*Deterministic REPEAT: only retains the first outcome; 
   9.161 @@ -246,10 +246,10 @@
   9.162    If non-negative, n bounds the number of repetitions.*)
   9.163  fun REPEAT_DETERM_N n tac = 
   9.164    let val tac = tracify trace_REPEAT tac
   9.165 -      fun drep 0 st = Some(st, Sequence.null)
   9.166 +      fun drep 0 st = Some(st, Seq.empty)
   9.167          | drep n st =
   9.168 -           (case Sequence.pull(tac st) of
   9.169 -                None       => Some(st, Sequence.null)
   9.170 +           (case Seq.pull(tac st) of
   9.171 +                None       => Some(st, Seq.empty)
   9.172                | Some(st',_) => drep (n-1) st')
   9.173    in  traced_tac (drep n)  end;
   9.174  
   9.175 @@ -260,11 +260,11 @@
   9.176  fun REPEAT tac = 
   9.177    let val tac = tracify trace_REPEAT tac
   9.178        fun rep qs st = 
   9.179 -        case Sequence.pull(tac st) of
   9.180 -            None       => Some(st, Sequence.seqof(fn()=> repq qs))
   9.181 +        case Seq.pull(tac st) of
   9.182 +            None       => Some(st, Seq.make(fn()=> repq qs))
   9.183            | Some(st',q) => rep (q::qs) st'
   9.184        and repq [] = None
   9.185 -        | repq(q::qs) = case Sequence.pull q of
   9.186 +        | repq(q::qs) = case Seq.pull q of
   9.187              None       => repq qs
   9.188            | Some(st,q) => rep (q::qs) st
   9.189    in  traced_tac (rep [])  end;
   9.190 @@ -277,12 +277,12 @@
   9.191  (** Filtering tacticals **)
   9.192  
   9.193  (*Returns all states satisfying the predicate*)
   9.194 -fun FILTER pred tac st = Sequence.filters pred (tac st);
   9.195 +fun FILTER pred tac st = Seq.filter pred (tac st);
   9.196  
   9.197  (*Returns all changed states*)
   9.198  fun CHANGED tac st = 
   9.199      let fun diff st' = not (eq_thm(st,st'))
   9.200 -    in  Sequence.filters diff (tac st)  end;
   9.201 +    in  Seq.filter diff (tac st)  end;
   9.202  
   9.203  
   9.204  (*** Tacticals based on subgoal numbering ***)
   9.205 @@ -320,7 +320,7 @@
   9.206  
   9.207  (*Make a tactic for subgoal i, if there is one.  *)
   9.208  fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
   9.209 -                             handle Subscript => Sequence.null;
   9.210 +                             handle Subscript => Seq.empty;
   9.211  
   9.212  
   9.213  (*** SELECT_GOAL ***)
   9.214 @@ -362,7 +362,7 @@
   9.215    let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
   9.216  	  eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
   9.217        fun next st = bicompose false (false, restore st, nprems_of st) i st0
   9.218 -  in  Sequence.flats (Sequence.maps next (tac eq_cprem))
   9.219 +  in  Seq.flat (Seq.map next (tac eq_cprem))
   9.220    end;
   9.221  
   9.222  (* (!!selct. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
   9.223 @@ -373,12 +373,12 @@
   9.224  (* Prevent the subgoal's assumptions from becoming additional subgoals in the
   9.225     new proof state by enclosing them by a universal quantification *)
   9.226  fun protect_subgoal st i =
   9.227 -        Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
   9.228 +        Seq.hd (bicompose false (false,dummy_quant_rl,1) i st)
   9.229          handle _ => error"SELECT_GOAL -- impossible error???";
   9.230  
   9.231  fun SELECT_GOAL tac i st = 
   9.232    case (i, List.drop(prems_of st, i-1)) of
   9.233 -      (_,[]) => Sequence.null
   9.234 +      (_,[]) => Seq.empty
   9.235      | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
   9.236      | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
   9.237      | (_, _::_) => select tac st i;
   9.238 @@ -489,7 +489,7 @@
   9.239        (*function to replace the current subgoal*)
   9.240        fun next st = bicompose false (false, relift st, nprems_of st)
   9.241                      i state
   9.242 -  in  Sequence.flats (Sequence.maps next (tacf subprems st0))
   9.243 +  in  Seq.flat (Seq.map next (tacf subprems st0))
   9.244    end;
   9.245  end;
   9.246  
    10.1 --- a/src/Pure/thm.ML	Fri Nov 21 15:26:22 1997 +0100
    10.2 +++ b/src/Pure/thm.ML	Fri Nov 21 15:27:43 1997 +0100
    10.3 @@ -19,8 +19,7 @@
    10.4    (*certified terms*)
    10.5    type cterm
    10.6    exception CTERM of string
    10.7 -  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ,
    10.8 -                                    maxidx: int}
    10.9 +  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
   10.10    val term_of           : cterm -> term
   10.11    val cterm_of          : Sign.sg -> term -> cterm
   10.12    val ctyp_of_term      : cterm -> ctyp
   10.13 @@ -121,7 +120,7 @@
   10.14    val equal_intr        : thm -> thm -> thm
   10.15    val equal_elim        : thm -> thm -> thm
   10.16    val implies_intr_hyps : thm -> thm
   10.17 -  val flexflex_rule     : thm -> thm Sequence.seq
   10.18 +  val flexflex_rule     : thm -> thm Seq.seq
   10.19    val instantiate       :
   10.20      (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
   10.21    val trivial           : cterm -> thm
   10.22 @@ -131,14 +130,14 @@
   10.23    val dest_state        : thm * int ->
   10.24      (term * term) list * term list * term * term
   10.25    val lift_rule         : (thm * int) -> thm -> thm
   10.26 -  val assumption        : int -> thm -> thm Sequence.seq
   10.27 +  val assumption        : int -> thm -> thm Seq.seq
   10.28    val eq_assumption     : int -> thm -> thm
   10.29    val rotate_rule       : int -> int -> thm -> thm
   10.30    val rename_params_rule: string list * int -> thm -> thm
   10.31    val bicompose         : bool -> bool * thm * int ->
   10.32 -    int -> thm -> thm Sequence.seq
   10.33 +    int -> thm -> thm Seq.seq
   10.34    val biresolution      : bool -> (bool * thm) list ->
   10.35 -    int -> thm -> thm Sequence.seq
   10.36 +    int -> thm -> thm Seq.seq
   10.37  
   10.38    (*meta simplification*)
   10.39    exception SIMPLIFIER of string * thm
   10.40 @@ -1016,7 +1015,7 @@
   10.41                       prop = newprop})
   10.42            end;
   10.43        val (tpairs,_) = Logic.strip_flexpairs prop
   10.44 -  in Sequence.maps newthm
   10.45 +  in Seq.map newthm
   10.46              (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
   10.47    end;
   10.48  
   10.49 @@ -1181,9 +1180,9 @@
   10.50                     Logic.rule_of (tpairs, Bs, C)
   10.51                 else (*normalize the new rule fully*)
   10.52                     Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
   10.53 -      fun addprfs [] = Sequence.null
   10.54 -        | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
   10.55 -             (Sequence.mapp newth
   10.56 +      fun addprfs [] = Seq.empty
   10.57 +        | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull
   10.58 +             (Seq.mapp newth
   10.59                  (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
   10.60                  (addprfs apairs)))
   10.61    in  addprfs (Logic.assum_pairs Bi)  end;
   10.62 @@ -1349,7 +1348,7 @@
   10.63    nsubgoal is the number of new subgoals (written m above).
   10.64    Curried so that resolution calls dest_state only once.
   10.65  *)
   10.66 -local open Sequence; exception COMPOSE
   10.67 +local exception COMPOSE
   10.68  in
   10.69  fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
   10.70                          (eres_flg, orule, nsubgoal) =
   10.71 @@ -1387,7 +1386,7 @@
   10.72                   shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
   10.73                   hyps = union_term(rhyps,shyps),
   10.74                   prop = Logic.rule_of normp}
   10.75 -        in  cons(th, thq)  end  handle COMPOSE => thq
   10.76 +        in  Seq.cons(th, thq)  end  handle COMPOSE => thq
   10.77       val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
   10.78       val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
   10.79         handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
   10.80 @@ -1403,23 +1402,23 @@
   10.81       val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
   10.82       val dpairs = BBi :: (rtpairs@stpairs);
   10.83       (*elim-resolution: try each assumption in turn.  Initially n=1*)
   10.84 -     fun tryasms (_, _, []) = null
   10.85 +     fun tryasms (_, _, []) = Seq.empty
   10.86         | tryasms (As, n, (t,u)::apairs) =
   10.87 -          (case pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
   10.88 +          (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
   10.89                 None                   => tryasms (As, n+1, apairs)
   10.90               | cell as Some((_,tpairs),_) =>
   10.91 -                   its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
   10.92 -                       (seqof (fn()=> cell),
   10.93 -                        seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
   10.94 +                   Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
   10.95 +                       (Seq.make (fn()=> cell),
   10.96 +                        Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs)))));
   10.97       fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
   10.98         | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
   10.99       (*ordinary resolution*)
  10.100 -     fun res(None) = null
  10.101 +     fun res(None) = Seq.empty
  10.102         | res(cell as Some((_,tpairs),_)) =
  10.103 -             its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  10.104 -                       (seqof (fn()=> cell), null)
  10.105 +             Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  10.106 +                       (Seq.make (fn()=> cell), Seq.empty)
  10.107   in  if eres_flg then eres(rev rAs)
  10.108 -     else res(pull(Unify.unifiers(sign, env, dpairs)))
  10.109 +     else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  10.110   end;
  10.111  end;  (*open Sequence*)
  10.112  
  10.113 @@ -1444,14 +1443,14 @@
  10.114          val B = Logic.strip_assums_concl Bi;
  10.115          val Hs = Logic.strip_assums_hyp Bi;
  10.116          val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
  10.117 -        fun res [] = Sequence.null
  10.118 +        fun res [] = Seq.empty
  10.119            | res ((eres_flg, rule)::brules) =
  10.120                if could_bires (Hs, B, eres_flg, rule)
  10.121 -              then Sequence.seqof (*delay processing remainder till needed*)
  10.122 +              then Seq.make (*delay processing remainder till needed*)
  10.123                    (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
  10.124                                 res brules))
  10.125                else res brules
  10.126 -    in  Sequence.flats (res brules)  end;
  10.127 +    in  Seq.flat (res brules)  end;
  10.128  
  10.129  
  10.130  
    11.1 --- a/src/Pure/unify.ML	Fri Nov 21 15:26:22 1997 +0100
    11.2 +++ b/src/Pure/unify.ML	Fri Nov 21 15:27:43 1997 +0100
    11.3 @@ -25,9 +25,9 @@
    11.4    val combound : (term*int*int) -> term
    11.5    val rlist_abs: (string*typ)list * term -> term   
    11.6    val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    11.7 -	-> (Envir.env Sequence.seq)
    11.8 +	-> (Envir.env Seq.seq)
    11.9    val unifiers: Sign.sg * Envir.env * ((term*term)list)
   11.10 -	-> (Envir.env * (term * term)list) Sequence.seq
   11.11 +	-> (Envir.env * (term * term)list) Seq.seq
   11.12    end;
   11.13  
   11.14  structure Unify	: UNIFY = 
   11.15 @@ -386,16 +386,16 @@
   11.16    The order for trying projections is crucial in ?b'(?a)   
   11.17    NB "vname" is only used in the call to make_args!!   *)
   11.18  fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   11.19 -	: (term * (Envir.env * dpair list))Sequence.seq =
   11.20 +	: (term * (Envir.env * dpair list))Seq.seq =
   11.21  let (*Produce copies of uarg and cons them in front of uargs*)
   11.22      fun copycons uarg (uargs, (env, dpairs)) =
   11.23 -	Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
   11.24 +	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
   11.25  	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
   11.26  		 (env, dpairs)));
   11.27  	(*Produce sequence of all possible ways of copying the arg list*)
   11.28 -    fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
   11.29 +    fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
   11.30        | copyargs (uarg::uargs) =
   11.31 -	    Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
   11.32 +	    Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
   11.33      val (uhead,uargs) = strip_comb u;
   11.34      val base = body_type env (fastype env (rbinder,uhead));
   11.35      fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
   11.36 @@ -404,7 +404,7 @@
   11.37      fun projenv (head, (Us,bary), targ, tail) = 
   11.38  	let val env = if !trace_types then test_unify_types(base,bary,env)
   11.39  		      else unify_types(base,bary,env)
   11.40 -	in Sequence.seqof (fn () =>  
   11.41 +	in Seq.make (fn () =>  
   11.42  	    let val (env',args) = make_args vname (Ts,env,Us);
   11.43  		(*higher-order projection: plug in targs for bound vars*)
   11.44  		fun plugin arg = list_comb(head_of arg, targs);
   11.45 @@ -413,7 +413,7 @@
   11.46  		    (*may raise exception CANTUNIFY*)
   11.47  	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   11.48  			tail)
   11.49 -	    end  handle CANTUNIFY => Sequence.pull tail)
   11.50 +	    end  handle CANTUNIFY => Seq.pull tail)
   11.51  	end handle CANTUNIFY => tail;
   11.52      (*make a list of projections*)
   11.53      fun make_projs (T::Ts, targ::targs) =
   11.54 @@ -425,12 +425,12 @@
   11.55  	       (projenv(bvar, strip_type env T, targ, matchfun projs))
   11.56        | matchfun [] = (*imitation last of all*)
   11.57  	      (case uhead of
   11.58 -		 Const _ => Sequence.maps joinargs (copyargs uargs)
   11.59 -	       | Free _  => Sequence.maps joinargs (copyargs uargs)
   11.60 -	       | _ => Sequence.null)  (*if Var, would be a loop!*)
   11.61 +		 Const _ => Seq.map joinargs (copyargs uargs)
   11.62 +	       | Free _  => Seq.map joinargs (copyargs uargs)
   11.63 +	       | _ => Seq.empty)  (*if Var, would be a loop!*)
   11.64  in case uhead of
   11.65  	Abs(a, T, body) =>
   11.66 -	    Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
   11.67 +	    Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 
   11.68  		(mc ((a,T)::rbinder,
   11.69  			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   11.70        | Var (w,uary) => 
   11.71 @@ -438,7 +438,7 @@
   11.72  	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   11.73  		val tabs = combound(newhd, 0, length Ts)
   11.74  		val tsub = list_comb(newhd,targs)
   11.75 -	    in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   11.76 +	    in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   11.77  	    end
   11.78        | _ =>  matchfun(rev(make_projs(Ts, targs)))
   11.79  end
   11.80 @@ -447,7 +447,7 @@
   11.81  
   11.82  (*Call matchcopy to produce assignments to the variable in the dpair*)
   11.83  fun MATCH (env, (rbinder,t,u), dpairs)
   11.84 -	: (Envir.env * dpair list)Sequence.seq = 
   11.85 +	: (Envir.env * dpair list)Seq.seq = 
   11.86    let val (Var(v,T), targs) = strip_comb t;
   11.87        val Ts = binder_types env T;
   11.88        fun new_dset (u', (env',dpairs')) =
   11.89 @@ -455,7 +455,7 @@
   11.90  	  case Envir.lookup(env',v) of
   11.91  	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   11.92  	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   11.93 -  in Sequence.maps new_dset
   11.94 +  in Seq.map new_dset
   11.95           (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   11.96    end;
   11.97  
   11.98 @@ -620,9 +620,9 @@
   11.99    Returns flex-flex disagreement pairs NOT IN normal form. 
  11.100    SIMPL may raise exception CANTUNIFY. *)
  11.101  fun hounifiers (sg,env, tus : (term*term)list) 
  11.102 -  : (Envir.env * (term*term)list)Sequence.seq =
  11.103 +  : (Envir.env * (term*term)list)Seq.seq =
  11.104    let fun add_unify tdepth ((env,dpairs), reseq) =
  11.105 -	  Sequence.seqof (fn()=>
  11.106 +	  Seq.make (fn()=>
  11.107  	  let val (env',flexflex,flexrigid) = 
  11.108  	       (if tdepth> !trace_bound andalso !trace_simp
  11.109  		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
  11.110 @@ -631,25 +631,25 @@
  11.111  	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
  11.112  	    | dp::frigid' => 
  11.113  		if tdepth > !search_bound then
  11.114 -		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
  11.115 +		    (prs"***Unification bound exceeded\n"; Seq.pull reseq)
  11.116  		else
  11.117  		(if tdepth > !trace_bound then
  11.118  		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
  11.119  		 else ();
  11.120 -		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
  11.121 +		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
  11.122  			   (MATCH (env',dp, frigid'@flexflex), reseq)))
  11.123  	  end
  11.124  	  handle CANTUNIFY => 
  11.125  	    (if tdepth > !trace_bound then writeln"Failure node" else ();
  11.126 -	     Sequence.pull reseq));
  11.127 +	     Seq.pull reseq));
  11.128       val dps = map (fn(t,u)=> ([],t,u)) tus
  11.129    in sgr := sg;
  11.130 -     add_unify 1 ((env,dps), Sequence.null) 
  11.131 +     add_unify 1 ((env,dps), Seq.empty) 
  11.132    end;
  11.133  
  11.134  fun unifiers(params) =
  11.135 -      Sequence.cons((Pattern.unify(params), []),   Sequence.null)
  11.136 -      handle Pattern.Unif => Sequence.null
  11.137 +      Seq.cons((Pattern.unify(params), []),   Seq.empty)
  11.138 +      handle Pattern.Unif => Seq.empty
  11.139             | Pattern.Pattern => hounifiers(params);
  11.140  
  11.141  
  11.142 @@ -682,7 +682,7 @@
  11.143    foldr smash_flexflex1 (tpairs, env);
  11.144  
  11.145  (*Returns unifiers with no remaining disagreement pairs*)
  11.146 -fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
  11.147 -    Sequence.maps smash_flexflex (unifiers(sg,env,tus));
  11.148 +fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
  11.149 +    Seq.map smash_flexflex (unifiers(sg,env,tus));
  11.150  
  11.151  end;