# HG changeset patch
# User wenzelm
# Date 938605767 -7200
# Node ID 838077e40a460480b196eee0b9fc04455cfcf848
# Parent  25a0d2ba3a87279532ad2ac89ee428fc090cf2a2
present sections;

diff -r 25a0d2ba3a87 -r 838077e40a46 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Sep 29 13:49:07 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Sep 29 13:49:27 1999 +0200
@@ -163,9 +163,13 @@
 fun add_text comment thy = thy:theory;
 fun add_title title author date thy = thy;
 val add_chapter = add_text;
-val add_section = add_text;
-val add_subsection = add_text;
-val add_subsubsection = add_text;
+
+fun gen_add_section add present txt thy =
+  (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy);
+
+val add_section = gen_add_section add_text Present.section;
+val add_subsection = gen_add_section add_text Present.subsection;
+val add_subsubsection = gen_add_section add_text Present.subsubsection;
 
 fun add_txt comment = ProofHistory.apply Proof.assert_forward;
 val add_sect = add_txt;