# HG changeset patch
# User paulson
# Date 827343657 -3600
# Node ID d89d5ff2397f0cdfa524fa39acf1f2fac3488838
# Parent  7fa0265dcd13ff36b43a32eff10f29a0d6517b43
maketest now closes the output file
Declared type mtree for proof objects

diff -r 7fa0265dcd13 -r d89d5ff2397f src/Pure/library.ML
--- 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;