--- a/src/Pure/Isar/toplevel.ML Thu Sep 09 18:17:34 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Sep 09 18:18:34 2010 +0200
@@ -30,7 +30,6 @@
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
val skip_proofs: bool Unsynchronized.ref
- exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
val thread: bool -> (unit -> unit) -> Thread.thread
type transition
@@ -222,8 +221,6 @@
val profiling = Unsynchronized.ref 0;
val skip_proofs = Unsynchronized.ref false;
-exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
-
fun program body =
(body
|> Runtime.controlled_execution