curried Seq.cons;
authorwenzelm
Wed Apr 26 22:38:16 2006 +0200 (2006-04-26)
changeset 194758aa2b380614a
parent 19474 70223ad97843
child 19476 816f519f8b72
curried Seq.cons;
src/Pure/General/seq.ML
src/Pure/IsaPlanner/focus_term_lib.ML
src/Pure/IsaPlanner/isa_fterm.ML
src/Pure/IsaPlanner/isaplib.ML
src/Pure/Isar/proof.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/General/seq.ML	Wed Apr 26 22:38:11 2006 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Wed Apr 26 22:38:16 2006 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val make: (unit -> ('a * 'a seq) option) -> 'a seq
     1.5    val pull: 'a seq -> ('a * 'a seq) option
     1.6    val empty: 'a seq
     1.7 -  val cons: 'a * 'a seq -> 'a seq
     1.8 +  val cons: 'a -> 'a seq -> 'a seq
     1.9    val single: 'a -> 'a seq
    1.10    val try: ('a -> 'b) -> 'a -> 'b seq
    1.11    val hd: 'a seq -> 'a
    1.12 @@ -70,9 +70,9 @@
    1.13  (*prefix an element to the sequence -- use cons (x, xq) only if
    1.14    evaluation of xq need not be delayed, otherwise use
    1.15    make (fn () => SOME (x, xq))*)
    1.16 -fun cons x_xq = make (fn () => SOME x_xq);
    1.17 +fun cons x xq = make (fn () => SOME (x, xq));
    1.18  
    1.19 -fun single x = cons (x, empty);
    1.20 +fun single x = cons x empty;
    1.21  
    1.22  (*head and tail -- beware of calling the sequence function twice!!*)
    1.23  fun hd xq = #1 (the (pull xq))
    1.24 @@ -101,7 +101,7 @@
    1.25    | SOME (x, xq') => x :: list_of xq');
    1.26  
    1.27  (*conversion from list to sequence*)
    1.28 -fun of_list xs = foldr cons empty xs;
    1.29 +fun of_list xs = fold_rev cons xs empty;
    1.30  
    1.31  
    1.32  (*sequence append:  put the elements of xq in front of those of yq*)
    1.33 @@ -239,6 +239,6 @@
    1.34  fun DETERM f x =
    1.35    (case pull (f x) of
    1.36      NONE => empty
    1.37 -  | SOME (x', _) => cons (x', empty));
    1.38 +  | SOME (x', _) => cons x' empty);
    1.39  
    1.40  end;
     2.1 --- a/src/Pure/IsaPlanner/focus_term_lib.ML	Wed Apr 26 22:38:11 2006 +0200
     2.2 +++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Wed Apr 26 22:38:16 2006 +0200
     2.3 @@ -334,7 +334,7 @@
     2.4      let 
     2.5        val botleft = (focus_bot_left_leaf in_t)
     2.6      in
     2.7 -      Seq.cons (botleft, (Seq.make (next_leaf_of_fcterm_seq_aux botleft)) )
     2.8 +      Seq.cons botleft (Seq.make (next_leaf_of_fcterm_seq_aux botleft))
     2.9      end;
    2.10  
    2.11    fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut;
     3.1 --- a/src/Pure/IsaPlanner/isa_fterm.ML	Wed Apr 26 22:38:11 2006 +0200
     3.2 +++ b/src/Pure/IsaPlanner/isa_fterm.ML	Wed Apr 26 22:38:16 2006 +0200
     3.3 @@ -339,7 +339,7 @@
     3.4  (* FIXME: make truly lazy *)
     3.5  fun focuseq_to_subgoals ft = 
     3.6      if (Logic.is_implies (focus_of_fcterm ft)) then 
     3.7 -      Seq.cons (focus_right (focus_left ft), focuseq_to_subgoals (focus_right ft))
     3.8 +      Seq.cons (focus_right (focus_left ft)) (focuseq_to_subgoals (focus_right ft))
     3.9      else
    3.10        Seq.empty;
    3.11  
     4.1 --- a/src/Pure/IsaPlanner/isaplib.ML	Wed Apr 26 22:38:11 2006 +0200
     4.2 +++ b/src/Pure/IsaPlanner/isaplib.ML	Wed Apr 26 22:38:16 2006 +0200
     4.3 @@ -143,7 +143,7 @@
     4.4  	    (case Seq.pull s2 of 
     4.5  	       NONE => NONE
     4.6  	     | SOME (a2,s3) => 
     4.7 -	       SOME (a, all_but_last_of_seq (Seq.cons (a2,s3))))
     4.8 +	       SOME (a, all_but_last_of_seq (Seq.cons a2 s3)))
     4.9      in
    4.10        Seq.make f
    4.11      end;
    4.12 @@ -178,7 +178,7 @@
    4.13              NONE => skipmore n
    4.14            | SOME (h,t) => 
    4.15              (case Seq.pull h of NONE => skip_occs n t
    4.16 -             | SOME _ => if n <= 1 then skipseq (Seq.cons (h, t))
    4.17 +             | SOME _ => if n <= 1 then skipseq (Seq.cons h t)
    4.18                           else skip_occs (n - 1) t)
    4.19      in (skip_occs m s) end;
    4.20  
     5.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 26 22:38:11 2006 +0200
     5.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 26 22:38:16 2006 +0200
     5.3 @@ -892,7 +892,7 @@
     5.4  fun check_result msg sq =
     5.5    (case Seq.pull sq of
     5.6      NONE => error msg
     5.7 -  | SOME res => Seq.cons res);
     5.8 +  | SOME (s', sq') => Seq.cons s' sq');
     5.9  
    5.10  fun global_qeds txt =
    5.11    end_proof true txt
     6.1 --- a/src/Pure/thm.ML	Wed Apr 26 22:38:11 2006 +0200
     6.2 +++ b/src/Pure/thm.ML	Wed Apr 26 22:38:16 2006 +0200
     6.3 @@ -1429,7 +1429,7 @@
     6.4                   hyps = union_hyps rhyps shyps,
     6.5                   tpairs = ntpairs,
     6.6                   prop = Logic.list_implies normp}
     6.7 -        in  Seq.cons(th, thq)  end  handle COMPOSE => thq;
     6.8 +        in  Seq.cons th thq  end  handle COMPOSE => thq;
     6.9       val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
    6.10         handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
    6.11       (*Modify assumptions, deleting n-th if n>0 for e-resolution*)