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;