# HG changeset patch
# User wenzelm
# Date 1552069348 -3600
# Node ID 45b2e784350ac79fbb95599b83d0471728210db1
# Parent  b49bd228ac8a79f8f5a367069bdec70595a2909d
tuned signature;

diff -r b49bd228ac8a -r 45b2e784350a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Mar 08 17:05:23 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Mar 08 19:22:28 2019 +0100
@@ -33,9 +33,11 @@
   val empty: transition
   val name_of: transition -> string
   val pos_of: transition -> Position.T
+  val timing_of: transition -> Time.time
   val type_error: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
+  val timing: Time.time -> transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
@@ -77,8 +79,6 @@
   val exec_id: Document_ID.exec -> transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val add_hook: (transition -> state -> state -> unit) -> unit
-  val get_timing: transition -> Time.time
-  val put_timing: Time.time -> transition -> transition
   val transition: bool -> transition -> state -> state * (exn * string) option
   val command_errors: bool -> transition -> state -> Runtime.error list * state option
   val command_exception: bool -> transition -> state -> state
@@ -327,6 +327,7 @@
 
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
+fun timing_of (Transition {timing, ...}) = timing;
 
 fun command_msg msg tr =
   msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^
@@ -344,6 +345,9 @@
 fun position pos = map_transition (fn (name, _, timing, trans) =>
   (name, pos, timing, trans));
 
+fun timing timing = map_transition (fn (name, pos, _, trans) =>
+  (name, pos, timing, trans));
+
 fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
   (name, pos, timing, tr :: trans));
 
@@ -582,9 +586,6 @@
 
 (* apply transitions *)
 
-fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans));
-
 local
 
 fun app int (tr as Transition {trans, ...}) =
@@ -678,7 +679,7 @@
 
 fun timing_estimate elem =
   let val trs = tl (Thy_Element.flat_element elem)
-  in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
+  in fold (fn tr => fn t => timing_of tr + t) trs Time.zeroTime end;
 
 fun future_proofs_enabled estimate st =
   (case try proof_of st of
diff -r b49bd228ac8a -r 45b2e784350a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Mar 08 17:05:23 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Mar 08 19:22:28 2019 +0100
@@ -285,7 +285,7 @@
     fun prepare_span st span =
       Command_Span.content span
       |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
-      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
+      |> (fn tr => Toplevel.timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
       let