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.";