src/Pure/Isar/toplevel.ML
changeset 61886 d4c89ea5e6dc
parent 61208 19118f9b939d
child 62239 6ee95b93fbed
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Dec 21 13:39:45 2015 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Dec 21 14:18:57 2015 +0100
     1.3 @@ -26,7 +26,6 @@
     1.4    val pretty_state: state -> Pretty.T list
     1.5    val string_of_state: state -> string
     1.6    val pretty_abstract: state -> Pretty.T
     1.7 -  val profiling: int Unsynchronized.ref
     1.8    type transition
     1.9    val empty: transition
    1.10    val name_of: transition -> string
    1.11 @@ -204,9 +203,6 @@
    1.12  
    1.13  (** toplevel transitions **)
    1.14  
    1.15 -val profiling = Unsynchronized.ref 0;
    1.16 -
    1.17 -
    1.18  (* node transactions -- maintaining stable checkpoints *)
    1.19  
    1.20  exception FAILURE of state * exn;
    1.21 @@ -568,10 +564,7 @@
    1.22    setmp_thread_position tr (fn state =>
    1.23      let
    1.24        val timing_start = Timing.start ();
    1.25 -
    1.26 -      val (result, opt_err) =
    1.27 -         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
    1.28 -
    1.29 +      val (result, opt_err) = apply_trans int trans state;
    1.30        val timing_result = Timing.result timing_start;
    1.31        val timing_props =
    1.32          Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);