# HG changeset patch
# User wenzelm
# Date 1737139256 -3600
# Node ID dc982cbeb54291c6db7e1159b55e991cd4dafaf2
# Parent  c712ecb5147454d8095479bcc3de98763a43f61b
clarified pattern matching;

diff -r c712ecb51474 -r dc982cbeb542 src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Fri Jan 17 19:30:26 2025 +0100
+++ b/src/HOL/Import/import_data.ML	Fri Jan 17 19:40:56 2025 +0100
@@ -82,12 +82,7 @@
 fun add_typ_def type_name abs_name rep_name th thy =
   let
     val th' = Thm.legacy_freezeT th
-    val ((_, rep), abs) =
-      Thm.prop_of th'
-      |> HOLogic.dest_Trueprop
-      |> dest_comb |> #1
-      |> dest_comb |>> dest_comb
-    val A = domain_type (fastype_of rep)
+    val \<^Const_>\<open>type_definition A _ for rep abs _\<close> = HOLogic.dest_Trueprop (Thm.prop_of th')
   in
     thy
     |> add_typ_map type_name (dest_Type_name A)