# 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;