add_title;

--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 11 21:53:36 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 11 21:53:50 1999 +0100
@@ -13,6 +13,7 @@
 signature ISAR_THY =
 sig
   val add_text: string -> theory -> theory
+  val add_title: string -> string -> string -> theory -> theory
   val add_chapter: string -> theory -> theory
   val add_section: string -> theory -> theory
   val add_subsection: string -> theory -> theory
@@ -74,6 +75,7 @@
 (* formal comments *)	(* FIXME dummy *)
 
 fun add_text (txt:string) (thy:theory) = thy;
+fun add_title title author date thy = thy;
 val add_chapter = add_text;
 val add_section = add_text;
 val add_subsection = add_text;