--- a/src/HOL/Data_Structures/Define_Time_Function.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sun Aug 04 17:39:47 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
@@ -610,8 +610,8 @@
(* Print result if print *)
val _ = if not print then () else
let
- val nms = map (fst o dest_Const) term
- val typs = map (snd o dest_Const) term
+ val nms = map dest_Const_name term
+ val typs = map dest_Const_type term
in
print_timing' print_ctxt { names=nms, terms=terms, typs=typs } (info_pfunc time_info)
end