# HG changeset patch
# User wenzelm
# Date 940941310 -7200
# Node ID fa6fec415492fdccfb782625759eb85d98c50d1e
# Parent  220892918bd1d9f8648342e039b1a033a8b00461
added kill_thy;

diff -r 220892918bd1 -r fa6fec415492 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 26 14:34:50 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 26 14:35:10 1999 +0200
@@ -15,6 +15,7 @@
   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_thy: string -> Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
@@ -71,6 +72,7 @@
 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);
+fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
 
 
 (* history commands *)
diff -r 220892918bd1 -r fa6fec415492 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 26 14:34:50 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 26 14:35:10 1999 +0200
@@ -562,6 +562,10 @@
   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
     (P.name >> IsarCmd.remove_thy);
 
+val kill_thyP =
+  OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
+    K.diag (P.name >> IsarCmd.kill_thy);
+
 val prP =
   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
     (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
@@ -574,16 +578,13 @@
   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
     (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
-
-val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
-
 val commitP =
   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
-    (opt_unit >> (K IsarCmd.use_commit));
+    (P.opt_unit >> (K IsarCmd.use_commit));
 
 val quitP =
   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
-    (opt_unit >> (K IsarCmd.quit));
+    (P.opt_unit >> (K IsarCmd.quit));
 
 val exitP =
   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
@@ -636,9 +637,9 @@
   print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
-  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, prP,
-  disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
-  welcomeP];
+  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
+  kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
+  init_toplevelP, welcomeP];
 
 
 end;