src/FOLP/ROOT.ML

--- a/src/FOLP/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
+++ b/src/FOLP/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
@@ -8,7 +8,5 @@
 Presence of unknown proof term means that matching does not behave as expected.
 *)
 
-val banner = "First-Order Logic with Natural Deduction with Proof Terms";
-writeln banner;
+use_thy "FOLP";
 
-use_thy "FOLP";