src/Pure/Isar/isar_cmd.ML

   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
   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
   val class_deps: Toplevel.transition -> Toplevel.transition
   val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition

       (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
     ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
       (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 =
   Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);