raw_t(e)xt: any proof mode;
authorwenzelm
Wed Dec 22 20:29:59 1999 +0100 (1999-12-22 ago)
changeset 8079ccfc64f29333
parent 8078 c6da7585f9d1
child 8080 908aca49c1a5
raw_t(e)xt: any proof mode;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Dec 22 20:29:36 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Dec 22 20:29:59 1999 +0100
     1.3 @@ -174,7 +174,7 @@
     1.4    Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
     1.5  
     1.6  fun add_text comment thy = thy:theory;
     1.7 -val add_text_raw = add_text;
     1.8 +fun add_text_raw _ x = x;
     1.9  val add_chapter = add_text;
    1.10  
    1.11  fun gen_add_section add present txt thy =
    1.12 @@ -185,7 +185,7 @@
    1.13  val add_subsubsection = gen_add_section add_text Present.subsubsection;
    1.14  
    1.15  fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    1.16 -val add_txt_raw = add_txt;
    1.17 +val add_txt_raw = add_text_raw;
    1.18  val add_sect = add_txt;
    1.19  val add_subsect = add_txt;
    1.20  val add_subsubsect = add_txt;