--- a/src/HOL/Library/refute.ML Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Library/refute.ML Sun Aug 04 13:24:54 2024 +0200
@@ -2180,7 +2180,7 @@
| Old_Datatype_Aux.DtRec i =>
let
val (_, ds, _) = the (AList.lookup (op =) descr i)
- val (_, Ts) = dest_Type T
+ val Ts = dest_Type_args T
in
rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
end)
@@ -2195,7 +2195,7 @@
val typ_assoc = filter
(fn (Old_Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
(rec_typ_assoc []
- (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
+ (#2 (the (AList.lookup (op =) descr idt_index)) ~~ dest_Type_args IDT))
(* sanity check: typ_assoc must associate types to the *)
(* elements of 'dtyps' (and only to those) *)
val _ =