src/Pure/basis.ML
changeset 2470 273580d5c040
parent 2402 b3d273ce5601
child 2862 3f38cbd57d47
     1.1 --- a/src/Pure/basis.ML	Fri Jan 03 15:01:55 1997 +0100
     1.2 +++ b/src/Pure/basis.ML	Fri Jan 03 15:25:51 1997 +0100
     1.3 @@ -100,3 +100,6 @@
     1.4    val output 	= output
     1.5    val flushOut 	= flush_out
     1.6    end;
     1.7 +
     1.8 +
     1.9 +fun print s = (output (std_out, s); flush_out std_out);