removed kill_theory;
authorwenzelm
Wed Sep 01 21:13:12 1999 +0200 (1999-09-01)
changeset 7413e25ad9ab0b50
parent 7412 35ebe1452c10
child 7414 9bc7797d1249
removed kill_theory;
print_thms: use Proof.pretty_thms;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 01 21:11:44 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 01 21:13:12 1999 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4    val touch_all_thys: Toplevel.transition -> Toplevel.transition
     1.5    val touch_thy: string -> Toplevel.transition -> Toplevel.transition
     1.6    val remove_thy: string -> Toplevel.transition -> Toplevel.transition
     1.7 -  val kill_theory: Toplevel.transition -> Toplevel.transition
     1.8    val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
     1.9    val clear_undo: Toplevel.transition -> Toplevel.transition
    1.10    val redo: Toplevel.transition -> Toplevel.transition
    1.11 @@ -67,7 +66,6 @@
    1.12  val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    1.13  fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    1.14  fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
    1.15 -val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
    1.16  
    1.17  
    1.18  (* history commands *)
    1.19 @@ -87,7 +85,7 @@
    1.20  val undo_theory = Toplevel.history (fn hist =>
    1.21    if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
    1.22  
    1.23 -val undo = kill_theory o undo_theory o undos_proof 1;
    1.24 +val undo = Toplevel.kill o undo_theory o undos_proof 1;
    1.25  
    1.26  
    1.27  (* use ML text *)
    1.28 @@ -148,7 +146,7 @@
    1.29  
    1.30  fun print_thms args = Toplevel.keep (fn state =>
    1.31    let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state
    1.32 -  in Display.print_thms (IsarThy.get_thmss args st) end);
    1.33 +  in Pretty.writeln (Proof.pretty_thms (IsarThy.get_thmss args st)) end);
    1.34  
    1.35  
    1.36  fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);