src/Pure/Isar/toplevel.ML
changeset 39237 be1acdcd55dc
parent 39232 69c6d3e87660
child 39285 85728a4b5620
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Sep 09 18:17:34 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Sep 09 18:18:34 2010 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4    val timing: bool Unsynchronized.ref
     1.5    val profiling: int Unsynchronized.ref
     1.6    val skip_proofs: bool Unsynchronized.ref
     1.7 -  exception TOPLEVEL_ERROR
     1.8    val program: (unit -> 'a) -> 'a
     1.9    val thread: bool -> (unit -> unit) -> Thread.thread
    1.10    type transition
    1.11 @@ -222,8 +221,6 @@
    1.12  val profiling = Unsynchronized.ref 0;
    1.13  val skip_proofs = Unsynchronized.ref false;
    1.14  
    1.15 -exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
    1.16 -
    1.17  fun program body =
    1.18   (body
    1.19    |> Runtime.controlled_execution