# HG changeset patch
# User wenzelm
# Date 1723027822 -7200
# Node ID c6dca9d3af4e99feff0e3c0c46a6a58ce260bf3f
# Parent  ebb1243098bf5651ea03f02e88371ad0ae3da02b
recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);

diff -r ebb1243098bf -r c6dca9d3af4e src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Wed Aug 07 11:58:45 2024 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Wed Aug 07 12:50:22 2024 +0200
@@ -543,9 +543,9 @@
     (* Print result if print *)
     val _ = if not print then () else
         let
-          val nms = map (fst o dest_Const) term
+          val nms = map dest_Const_name term
           val used = map (used_for_const orig_used) term
-          val typs = map (snd o dest_Const) term
+          val typs = map dest_Const_type term
         in
           print_timing' print_ctxt { names=nms, terms=terms, typs=typs } { names=timing_names, terms=T_terms, typs=map (fn (used, typ) => change_typ' used 0 typ) (zip used typs) }
         end