# HG changeset patch
# User wenzelm
# Date 936213192 -7200
# Node ID e25ad9ab0b508b0208f65987b2002895eabd7c99
# Parent  35ebe1452c1017f1f2705ab8ee207fd76c7d86df
removed kill_theory;
print_thms: use Proof.pretty_thms;

diff -r 35ebe1452c10 -r e25ad9ab0b50 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 01 21:11:44 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 01 21:13:12 1999 +0200
@@ -13,7 +13,6 @@
   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
@@ -67,7 +66,6 @@
 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 *)
@@ -87,7 +85,7 @@
 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 *)
@@ -148,7 +146,7 @@
 
 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);