# HG changeset patch
# User wenzelm
# Date 945890999 -3600
# Node ID ccfc64f293335b5328d6d5c0c5fce9083bcbf1e5
# Parent  c6da7585f9d1f55478bbc06a9efb84a78e594e5b
raw_t(e)xt: any proof mode;

diff -r c6da7585f9d1 -r ccfc64f29333 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Dec 22 20:29:36 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Dec 22 20:29:59 1999 +0100
@@ -174,7 +174,7 @@
   Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
 
 fun add_text comment thy = thy:theory;
-val add_text_raw = add_text;
+fun add_text_raw _ x = x;
 val add_chapter = add_text;
 
 fun gen_add_section add present txt thy =
@@ -185,7 +185,7 @@
 val add_subsubsection = gen_add_section add_text Present.subsubsection;
 
 fun add_txt comment = ProofHistory.apply Proof.assert_forward;
-val add_txt_raw = add_txt;
+val add_txt_raw = add_text_raw;
 val add_sect = add_txt;
 val add_subsect = add_txt;
 val add_subsubsect = add_txt;