# HG changeset patch
# User wenzelm
# Date 1014666660 -3600
# Node ID 8a1147c57575c4e85ff786218377d90349a58d44
# Parent  26c0566adf62b7de0a4af4d8cae9968a364c9965
markup commands moved to isar_cmd.ML;

diff -r 26c0566adf62 -r 8a1147c57575 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Feb 25 20:50:42 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Feb 25 20:51:00 2002 +0100
@@ -8,18 +8,6 @@
 
 signature ISAR_THY =
 sig
-  val add_header: string -> Toplevel.transition -> Toplevel.transition
-  val add_chapter: string -> theory -> theory
-  val add_section: string -> theory -> theory
-  val add_subsection: string -> theory -> theory
-  val add_subsubsection: string -> theory -> theory
-  val add_text: string -> theory -> theory
-  val add_text_raw: string -> theory -> theory
-  val add_sect: string -> ProofHistory.T -> ProofHistory.T
-  val add_subsect: string -> ProofHistory.T -> ProofHistory.T
-  val add_subsubsect: string -> ProofHistory.T -> ProofHistory.T
-  val add_txt: string -> ProofHistory.T -> ProofHistory.T
-  val add_txt_raw: string -> ProofHistory.T -> ProofHistory.T
   val hide_space: string * xstring list -> theory -> theory
   val hide_space_i: string * string list -> theory -> theory
   val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
@@ -174,28 +162,6 @@
 
 (** derived theory and proof operations **)
 
-(* markup commands *)
-
-fun add_header x =
-  Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
-
-fun add_text _ x = x;
-fun add_text_raw _ x = x;
-
-fun add_heading add present txt thy = (Context.setmp (Some thy) present txt; add txt thy);
-
-val add_chapter = add_heading add_text Present.section;
-val add_section = add_heading add_text Present.section;
-val add_subsection = add_heading add_text Present.subsection;
-val add_subsubsection = add_heading add_text Present.subsubsection;
-
-fun add_txt (_: string) = ProofHistory.apply I;
-val add_txt_raw = add_txt;
-val add_sect = add_txt;
-val add_subsect = add_txt;
-val add_subsubsect = add_txt;
-
-
 (* name spaces *)
 
 local