# HG changeset patch
# User wenzelm
# Date 932156606 -7200
# Node ID 5d1eafaff50cf6a87c016edc52a7a47368c08dbf
# Parent  abf9d5e2fb6e0db029c9ba924eea32609c851f81
removed break;

diff -r abf9d5e2fb6e -r 5d1eafaff50c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 16 22:22:59 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Jul 16 22:23:26 1999 +0200
@@ -7,7 +7,6 @@
 
 signature ISAR_CMD =
 sig
-  val break: Toplevel.transition -> Toplevel.transition
   val exit: Toplevel.transition -> Toplevel.transition
   val restart: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
@@ -47,8 +46,6 @@
 
 (* variations on exit *)
 
-val break = Toplevel.keep (fn state => raise Toplevel.BREAK state);
-
 val exit = Toplevel.keep (fn state =>
   (Context.set_context (try Toplevel.theory_of state);
     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
diff -r abf9d5e2fb6e -r 5d1eafaff50c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jul 16 22:22:59 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 16 22:23:26 1999 +0200
@@ -524,10 +524,6 @@
   OuterSyntax.improper_command "restart" "restart Isar loop" K.control
     (Scan.succeed IsarCmd.restart);
 
-val breakP =
-  OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
-    (Scan.succeed IsarCmd.break);
-
 
 
 (** the Pure outer syntax **)
@@ -564,7 +560,7 @@
   print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
-  quitP, exitP, restartP, breakP];
+  quitP, exitP, restartP];
 
 
 end;