diff -r a1a8248a4677 -r 802576856527 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:04:46 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:34:29 2013 +0200
@@ -39,8 +39,6 @@
   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
-  val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
-  val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
   val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
@@ -275,21 +273,6 @@
       (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
 
 
-(* present draft files *)
-
-fun display_drafts names = Toplevel.imperative (fn () =>
-  let
-    val paths = map Path.explode names;
-    val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths);
-  in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
-
-fun print_drafts names = Toplevel.imperative (fn () =>
-  let
-    val paths = map Path.explode names;
-    val outfile = File.shell_path (Present.drafts "ps" paths);
-  in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
-
-
 (* print theorems *)
 
 val print_theorems_proof =