src/Pure/display.ML
changeset 4270 957c887b89b5
parent 4256 e768c42069bb
child 4440 9ed4098074bc
     1.1 --- a/src/Pure/display.ML	Fri Nov 21 15:26:22 1997 +0100
     1.2 +++ b/src/Pure/display.ML	Fri Nov 21 15:27:43 1997 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4    val print_data	: theory -> string -> unit
     1.5    val print_thm		: thm -> unit
     1.6    val prth		: thm -> thm
     1.7 -  val prthq		: thm Sequence.seq -> thm Sequence.seq
     1.8 +  val prthq		: thm Seq.seq -> thm Seq.seq
     1.9    val prths		: thm list -> thm list
    1.10    val show_hyps		: bool ref
    1.11    val string_of_cterm	: cterm -> string
    1.12 @@ -67,7 +67,7 @@
    1.13  
    1.14  (*Print and return a sequence of theorems, separated by blank lines. *)
    1.15  fun prthq thseq =
    1.16 -  (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
    1.17 +  (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
    1.18  
    1.19  (*Print and return a list of theorems, separated by blank lines. *)
    1.20  fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths);