# HG changeset patch
# User wenzelm
# Date 1723031137 -7200
# Node ID 2191ad2d684e2db917ddee4ae31d92a2aedba26e
# Parent  46eb1135f9bd9ac0761b349c173d748ea378b34b
clarified: more robust (dest_Type_name o body_type), which may fail in both parts;

diff -r 46eb1135f9bd -r 2191ad2d684e src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Aug 07 13:25:51 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Aug 07 13:45:37 2024 +0200
@@ -63,19 +63,17 @@
   let
     val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
   in
-    (case body_type T of
-      Type (tyco, _) => AList.lookup (op =) tab tyco
-    | _ => NONE)
+    try (dest_Type_name o body_type) T
+    |> Option.mapPartial (AList.lookup (op =) tab)
   end;
 
 fun info_of_constr_permissive thy (c, T) =
   let
     val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
-    val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
     val default = if null tab then NONE else SOME (snd (List.last tab));
     (*conservative wrt. overloaded constructors*)
   in
-    (case hint of
+    (case try (dest_Type_name o body_type) T of
       NONE => default
     | SOME tyco =>
         (case AList.lookup (op =) tab tyco of