kill: include kill_proof;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Mar 17 16:29:35 2000 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Mar 17 16:30:03 2000 +0100
@@ -27,6 +27,7 @@
   val kill_proof: Toplevel.transition -> Toplevel.transition
   val undo_theory: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
+  val kill: Toplevel.transition -> Toplevel.transition
   val use: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
@@ -114,6 +115,7 @@
   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
 
 val undo = Toplevel.kill o undo_theory o undos_proof 1;
+val kill = Toplevel.kill o kill_proof;
 
 
 (* use ML text *)
@@ -175,8 +177,13 @@
 (* print theorems / types / terms / props *)
 
 fun print_thms (ms, args) = Toplevel.keep (fn state =>
-  let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state
-  in with_modes ms (fn () => Pretty.writeln (Proof.pretty_thms (IsarThy.get_thmss args st))) end);
+  let
+    val st = Toplevel.node_case Proof.init_state Proof.enter_forward state;
+    val transfer = Thm.transfer (Toplevel.theory_of state);
+  in
+    with_modes ms (fn () =>
+      Pretty.writeln (Proof.pretty_thms (map transfer (IsarThy.get_thmss args st))))
+  end);
 
 fun print_type (ms, s) = Toplevel.keep (fn state =>
   let