# HG changeset patch
# User wenzelm
# Date 925488409 -7200
# Node ID 28553eba1913ada32636bc1548ebf60484fa4401
# Parent  de4047b0301736171d3e786a03b64c0bafaf7c6a
Comment.text;

diff -r de4047b03017 -r 28553eba1913 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Apr 30 18:06:35 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 30 18:06:49 1999 +0200
@@ -11,12 +11,12 @@
 
 signature ISAR_THY =
 sig
-  val add_text: string -> theory -> theory
-  val add_title: string -> string -> string -> theory -> theory
-  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: Comment.text -> theory -> theory
+  val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
+  val add_chapter: Comment.text -> theory -> theory
+  val add_section: Comment.text -> theory -> theory
+  val add_subsection: Comment.text -> theory -> theory
+  val add_subsubsection: Comment.text -> theory -> theory
   val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
   val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
@@ -105,7 +105,7 @@
 
 (* formal comments *)   (* FIXME dummy *)
 
-fun add_text (txt:string) (thy:theory) = thy;
+fun add_text _ thy = thy;
 fun add_title title author date thy = thy;
 val add_chapter = add_text;
 val add_section = add_text;