src/Pure/drule.ML
changeset 4270 957c887b89b5
parent 4057 edd8cb346109
child 4281 6c6073b13600
     1.1 --- a/src/Pure/drule.ML	Fri Nov 21 15:26:22 1997 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Nov 21 15:27:43 1997 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4  
     1.5  (*Resolution: exactly one resolvent must be produced.*)
     1.6  fun tha RSN (i,thb) =
     1.7 -  case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
     1.8 +  case Seq.chop (2, biresolution false [(false,tha)] i thb) of
     1.9        ([th],_) => th
    1.10      | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
    1.11      |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
    1.12 @@ -267,7 +267,7 @@
    1.13  (*For joining lists of rules*)
    1.14  fun thas RLN (i,thbs) =
    1.15    let val resolve = biresolution false (map (pair false) thas) i
    1.16 -      fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
    1.17 +      fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
    1.18    in  List.concat (map resb thbs)  end;
    1.19  
    1.20  fun thas RL thbs = thas RLN (1,thbs);
    1.21 @@ -289,7 +289,7 @@
    1.22    with no lifting or renaming!  Q may contain ==> or meta-quants
    1.23    ALWAYS deletes premise i *)
    1.24  fun compose(tha,i,thb) =
    1.25 -    Sequence.list_of_s (bicompose false (false,tha,0) i thb);
    1.26 +    Seq.list_of (bicompose false (false,tha,0) i thb);
    1.27  
    1.28  (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
    1.29  fun tha COMP thb =