src/Pure/Isar/isar_thy.ML
changeset 7633 838077e40a46
parent 7614 88392b7bc549
child 7666 226ea33c7cd6
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Sep 29 13:49:07 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Sep 29 13:49:27 1999 +0200
     1.3 @@ -163,9 +163,13 @@
     1.4  fun add_text comment thy = thy:theory;
     1.5  fun add_title title author date thy = thy;
     1.6  val add_chapter = add_text;
     1.7 -val add_section = add_text;
     1.8 -val add_subsection = add_text;
     1.9 -val add_subsubsection = add_text;
    1.10 +
    1.11 +fun gen_add_section add present txt thy =
    1.12 +  (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy);
    1.13 +
    1.14 +val add_section = gen_add_section add_text Present.section;
    1.15 +val add_subsection = gen_add_section add_text Present.subsection;
    1.16 +val add_subsubsection = gen_add_section add_text Present.subsubsection;
    1.17  
    1.18  fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    1.19  val add_sect = add_txt;