src/Pure/drule.ML
changeset 4270 957c887b89b5
parent 4057 edd8cb346109
child 4281 6c6073b13600
--- 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 =