# HG changeset patch
# User wenzelm
# Date 1146083896 -7200
# Node ID 8aa2b380614a2f710a67f87616c1bc188b9342de
# Parent  70223ad978430f5522badcc3ad5fa8e5d85a4834
curried Seq.cons;

diff -r 70223ad97843 -r 8aa2b380614a src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/General/seq.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -14,7 +14,7 @@
   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 cons: 'a -> 'a seq -> 'a seq
   val single: 'a -> 'a seq
   val try: ('a -> 'b) -> 'a -> 'b seq
   val hd: 'a seq -> 'a
@@ -70,9 +70,9 @@
 (*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 cons x xq = make (fn () => SOME (x, xq));
 
-fun single x = cons (x, empty);
+fun single x = cons x empty;
 
 (*head and tail -- beware of calling the sequence function twice!!*)
 fun hd xq = #1 (the (pull xq))
@@ -101,7 +101,7 @@
   | SOME (x, xq') => x :: list_of xq');
 
 (*conversion from list to sequence*)
-fun of_list xs = foldr cons empty xs;
+fun of_list xs = fold_rev cons xs empty;
 
 
 (*sequence append:  put the elements of xq in front of those of yq*)
@@ -239,6 +239,6 @@
 fun DETERM f x =
   (case pull (f x) of
     NONE => empty
-  | SOME (x', _) => cons (x', empty));
+  | SOME (x', _) => cons x' empty);
 
 end;
diff -r 70223ad97843 -r 8aa2b380614a src/Pure/IsaPlanner/focus_term_lib.ML
--- a/src/Pure/IsaPlanner/focus_term_lib.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -334,7 +334,7 @@
     let 
       val botleft = (focus_bot_left_leaf in_t)
     in
-      Seq.cons (botleft, (Seq.make (next_leaf_of_fcterm_seq_aux botleft)) )
+      Seq.cons botleft (Seq.make (next_leaf_of_fcterm_seq_aux botleft))
     end;
 
   fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut;
diff -r 70223ad97843 -r 8aa2b380614a src/Pure/IsaPlanner/isa_fterm.ML
--- a/src/Pure/IsaPlanner/isa_fterm.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/IsaPlanner/isa_fterm.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -339,7 +339,7 @@
 (* FIXME: make truly lazy *)
 fun focuseq_to_subgoals ft = 
     if (Logic.is_implies (focus_of_fcterm ft)) then 
-      Seq.cons (focus_right (focus_left ft), focuseq_to_subgoals (focus_right ft))
+      Seq.cons (focus_right (focus_left ft)) (focuseq_to_subgoals (focus_right ft))
     else
       Seq.empty;
 
diff -r 70223ad97843 -r 8aa2b380614a src/Pure/IsaPlanner/isaplib.ML
--- a/src/Pure/IsaPlanner/isaplib.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/IsaPlanner/isaplib.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -143,7 +143,7 @@
 	    (case Seq.pull s2 of 
 	       NONE => NONE
 	     | SOME (a2,s3) => 
-	       SOME (a, all_but_last_of_seq (Seq.cons (a2,s3))))
+	       SOME (a, all_but_last_of_seq (Seq.cons a2 s3)))
     in
       Seq.make f
     end;
@@ -178,7 +178,7 @@
             NONE => skipmore n
           | SOME (h,t) => 
             (case Seq.pull h of NONE => skip_occs n t
-             | SOME _ => if n <= 1 then skipseq (Seq.cons (h, t))
+             | SOME _ => if n <= 1 then skipseq (Seq.cons h t)
                          else skip_occs (n - 1) t)
     in (skip_occs m s) end;
 
diff -r 70223ad97843 -r 8aa2b380614a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -892,7 +892,7 @@
 fun check_result msg sq =
   (case Seq.pull sq of
     NONE => error msg
-  | SOME res => Seq.cons res);
+  | SOME (s', sq') => Seq.cons s' sq');
 
 fun global_qeds txt =
   end_proof true txt
diff -r 70223ad97843 -r 8aa2b380614a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/thm.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -1429,7 +1429,7 @@
                  hyps = union_hyps rhyps shyps,
                  tpairs = ntpairs,
                  prop = Logic.list_implies normp}
-        in  Seq.cons(th, thq)  end  handle COMPOSE => thq;
+        in  Seq.cons th thq  end  handle COMPOSE => thq;
      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)