diff -r b1861768d8f4 -r 8f3099589cfa src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:46 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:48 2007 +0200
@@ -21,7 +21,7 @@
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
   val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
-  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
+  val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
   val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
     Proof.context -> 'a list -> string
@@ -286,7 +286,7 @@
 end;
 
 
-(* present_thy *)
+(* process_thy *)
 
 datatype markup = Markup | MarkupEnv | Verbatim;
 
@@ -317,7 +317,7 @@
 
 in
 
-fun present_thy lex default_tags is_markup trs src =
+fun process_thy lex default_tags is_markup trs src =
   let
     (* tokens *)