# HG changeset patch
# User wenzelm
# Date 1121362101 -7200
# Node ID d7b47195ac7bf6af0bd0fc1b4aa99079ef76ead3
# Parent  131ca99f6abfb22e0e1466bb823f3c36b8bb9c20
proper structure;

diff -r 131ca99f6abf -r d7b47195ac7b src/HOL/Tools/ATP/VampireCommunication.ML
--- a/src/HOL/Tools/ATP/VampireCommunication.ML	Thu Jul 14 19:28:20 2005 +0200
+++ b/src/HOL/Tools/ATP/VampireCommunication.ML	Thu Jul 14 19:28:21 2005 +0200
@@ -1,10 +1,11 @@
-(*  Title:      VampireCommunication.ml
+(*  Title:      VampireCommunication.ML
     ID:         $Id$
     Author:     Claire Quigley
     Copyright   2004  University of Cambridge
 *)
 
-(* FIXME proper structure definition *)
+structure VampireCommunication =
+struct
 
 (***************************************************************************)
 (*  Code to deal with the transfer of proofs from a Vampire process        *)
@@ -109,3 +110,5 @@
     else
       (Pretty.writeln (Pretty.str (concat ["vampire", thisLine])); getVampInput instr)
   end;
+
+end;