# HG changeset patch
# User wenzelm
# Date 1737110867 -3600
# Node ID f9d0d2ca2402340720e26d4de8571b498804cd2c
# Parent  4329a8fecbe151a203358d36302b478de6fcc9b7
unused;

diff -r 4329a8fecbe1 -r f9d0d2ca2402 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 11:24:40 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 11:47:47 2025 +0100
@@ -353,14 +353,6 @@
     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