src/Pure/Isar/isar_cmd.ML
changeset 7023 5d1eafaff50c
parent 7012 ae9dac5af9d1
child 7101 ee79bf6feee2
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 16 22:22:59 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Jul 16 22:23:26 1999 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature ISAR_CMD =
     1.6  sig
     1.7 -  val break: Toplevel.transition -> Toplevel.transition
     1.8    val exit: Toplevel.transition -> Toplevel.transition
     1.9    val restart: Toplevel.transition -> Toplevel.transition
    1.10    val quit: Toplevel.transition -> Toplevel.transition
    1.11 @@ -47,8 +46,6 @@
    1.12  
    1.13  (* variations on exit *)
    1.14  
    1.15 -val break = Toplevel.keep (fn state => raise Toplevel.BREAK state);
    1.16 -
    1.17  val exit = Toplevel.keep (fn state =>
    1.18    (Context.set_context (try Toplevel.theory_of state);
    1.19      writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";