--- 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 =