# HG changeset patch
# User wenzelm
# Date 882521844 -3600
# Node ID 54f4fbc77c6ce0005d07e42e876aac2b241cd8cd
# Parent  a3a683a8bcc65e48dfdb984a283927aa9c037a42
removed maketest;

diff -r a3a683a8bcc6 -r 54f4fbc77c6c src/Pure/Thy/file.ML
--- a/src/Pure/Thy/file.ML	Thu Dec 18 19:12:22 1997 +0100
+++ b/src/Pure/Thy/file.ML	Fri Dec 19 09:57:24 1997 +0100
@@ -5,14 +5,8 @@
 File system operations.
 *)
 
-signature BASIC_FILE =
-sig
-  val maketest: string -> unit
-end;
-
 signature FILE =
 sig
-  include BASIC_FILE
   val tmp_name: string -> string
   val exists: string -> bool
   val info: string -> string
@@ -67,13 +61,4 @@
   else write outfile (read infile);
 
 
-(*for the "test" target in IsaMakefiles -- signifies successful termination*)
-fun maketest msg =
-  (writeln msg; write "test" "Test examples ran successfully\n");
-
-
 end;
-
-
-structure BasicFile: BASIC_FILE = File;
-open BasicFile;