# HG changeset patch
# User wenzelm
# Date 1450703937 -3600
# Node ID d4c89ea5e6dc9bd8cffbe063f4b334566e85bef9
# Parent  c0f34fe6aa613a62981843914ef59bad3165cfdb
discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);

diff -r c0f34fe6aa61 -r d4c89ea5e6dc src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Dec 21 13:39:45 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Dec 21 14:18:57 2015 +0100
@@ -26,7 +26,6 @@
   val pretty_state: state -> Pretty.T list
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
-  val profiling: int Unsynchronized.ref
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -204,9 +203,6 @@
 
 (** toplevel transitions **)
 
-val profiling = Unsynchronized.ref 0;
-
-
 (* node transactions -- maintaining stable checkpoints *)
 
 exception FAILURE of state * exn;
@@ -568,10 +564,7 @@
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
-
-      val (result, opt_err) =
-         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-
+      val (result, opt_err) = apply_trans int trans state;
       val timing_result = Timing.result timing_start;
       val timing_props =
         Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);