# HG changeset patch
# User wenzelm
# Date 918764299 -3600
# Node ID 55e5bc91ae22bed92306fe7cfde3a5aade86b76a
# Parent  94ce639eb7e58d6023a6405ce072e78bf2b53b47
init, finish;

diff -r 94ce639eb7e5 -r 55e5bc91ae22 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Feb 11 21:17:10 1999 +0100
+++ b/src/Pure/Thy/present.ML	Thu Feb 11 21:18:19 1999 +0100
@@ -13,13 +13,20 @@
 signature PRESENT =
 sig
   include BASIC_PRESENT
+  val init: bool -> string list -> string list -> string -> string -> unit
+  val finish: unit -> unit
+  val theory_file: string -> string -> unit
   val thm: string -> thm -> unit
 end;
 
 structure Present: PRESENT =
 struct
 
+fun init _ _ _ _ _ = ();
+fun finish _ = ();
+
 fun section _ = ();
+fun theory_file _ _ = ();
 fun thm _ _ = ();
 
 end;