src/Pure/Isar/isar_cmd.ML

   val quit: Toplevel.transition -> Toplevel.transition
   val init_toplevel: Toplevel.transition -> Toplevel.transition
   val touch_all_thys: Toplevel.transition -> Toplevel.transition
   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
-  val kill_theory: Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val clear_undo: Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
   val kill_proof: Toplevel.transition -> Toplevel.transition

 (* touch theories *)
 
 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
-val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
 
 
 (* history commands *)
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));

   | Toplevel.Proof _ => History.undo hist));
 
 val undo_theory = Toplevel.history (fn hist =>
   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
 
-val undo = kill_theory o undo_theory o undos_proof 1;
+val undo = Toplevel.kill o undo_theory o undos_proof 1;
 
 
 (* use ML text *)
 
 fun use name = Toplevel.keep (fn state =>

 
 (* print theorems / types / terms / props *)
 
 fun print_thms args = Toplevel.keep (fn state =>
   let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state
-  in Display.print_thms (IsarThy.get_thmss args st) end);
+  in Pretty.writeln (Proof.pretty_thms (IsarThy.get_thmss args st)) end);
 
 
 fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);
 
 fun read_term T thy s =