diff -r 0a5f598cacec -r 93b558e05f21 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Jul 27 12:43:58 2012 +0200
+++ b/src/Pure/System/session.ML	Fri Jul 27 13:01:19 2012 +0200
@@ -11,7 +11,7 @@
   val welcome: unit -> string
   val finish: unit -> unit
   val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
-    string -> string -> string * string -> string -> bool -> unit
+    string -> string -> string * Present.dump_mode -> string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
@@ -112,7 +112,7 @@
 
 local
 
-fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty");
+fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
 
 in