src/HOL/Import/import_rule.ML

     val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
   in
     snd (Global_Theory.add_thm ((binding, thm'), []) thy)
   end
 
+fun log_timestamp () =
+  let
+    val time = Time.now ()
+    val millis = nth (space_explode "." (Time.fmt 3 time)) 1
+  in
+    Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
+  end
+
 fun process_line str tstate =
   let
     fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
       | process tstate (#"B", [t]) = gettm t tstate |>> beta |-> setth
       | process tstate (#"1", [th]) = getth th tstate |>> conj1 |-> setth

           gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm
       | process tstate (#"l", [t1, t2]) =
           gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
       | process (thy, state) (#"+", [s]) =
           let
-            val _ = tracing ("Noting: " ^ s)
+            val _ = tracing ("NOTING " ^ log_timestamp () ^ ": " ^ s)
           in
             (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
           end
       | process _ (c, _) = error ("process: unknown command: " ^ String.implode [c])