# HG changeset patch
# User wenzelm
# Date 939130616 -7200
# Node ID 9c098c777926bd6f0c1a645dccdcbb11d3207030
# Parent  a469d66aa41758f73e8bdc35693ca5abc0a548cc
replace add_title by add_header;

diff -r a469d66aa417 -r 9c098c777926 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Oct 05 15:36:28 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Oct 05 15:36:56 1999 +0200
@@ -7,7 +7,7 @@
 
 signature ISAR_THY =
 sig
-  val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
+  val add_header: Comment.text -> Toplevel.transition -> Toplevel.transition
   val add_chapter: Comment.text -> theory -> theory
   val add_section: Comment.text -> theory -> theory
   val add_subsection: Comment.text -> theory -> theory
@@ -166,8 +166,10 @@
 
 (* formal comments *)
 
+fun add_header comment =
+  Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
+
 fun add_text comment thy = thy:theory;
-fun add_title title author date thy = thy;
 val add_chapter = add_text;
 
 fun gen_add_section add present txt thy =
@@ -512,10 +514,7 @@
 
 val begin_theory = gen_begin_theory ThyInfo.begin_theory;
 val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
-
-fun end_theory thy =
-  (Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);
-
+val end_theory = ThyInfo.end_theory;
 fun kill_theory thy = ThyInfo.remove_thy (PureThy.get_name thy);