src/Pure/Isar/isar_syn.ML

     (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "display_drafts"}
     "display raw source files with symbols"
-    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
-
-val _ =
-  Outer_Syntax.improper_command @{command_spec "print_drafts"}
-    "print raw source files with symbols"
-    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
+    (Scan.repeat1 Parse.path >> (fn names =>
+      Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_state"}
     "print current proof state (if present)"
     (opt_modes >> (fn modes =>