--- a/src/Pure/library.ML Wed Mar 20 18:39:59 1996 +0100
+++ b/src/Pure/library.ML Wed Mar 20 18:40:57 1996 +0100
@@ -730,10 +730,13 @@
else error (msg_fn x)
in asl l end;
-(* FIXME close file (?) *)
(*for the "test" target in Makefiles -- signifies successful termination*)
fun maketest msg =
- (writeln msg; output (open_out "test", "Test examples ran successfully\n"));
+ (writeln msg;
+ let val os = open_out "test"
+ in output (os, "Test examples ran successfully\n");
+ close_out os
+ end);
(*print a list surrounded by the brackets lpar and rpar, with comma separator
@@ -946,4 +949,7 @@
end;
+(*Variable-branching trees: for proof terms*)
+datatype 'a mtree = Join of 'a * 'a mtree list;
+
open Library;