# HG changeset patch
# User wenzelm
# Date 1737474646 -3600
# Node ID 4ae4ab4e454d3786166064478e59b67706c744eb
# Parent  da3c3948a39c6a76cdf9d92a882be69d2e05e0ee
more robust: explicit check for "Trueprop";

diff -r da3c3948a39c -r 4ae4ab4e454d src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Tue Jan 21 16:22:15 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Tue Jan 21 16:50:46 2025 +0100
@@ -80,7 +80,7 @@
 
 fun eq_mp th1 th2 =
   let
-    val (Q, P) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1))
+    val (Q, P) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th1))
     val i1 = Thm.instantiate' [] [SOME Q, SOME P] @{thm iffD1}
     val i2 = meta_mp i1 th1
   in
@@ -89,8 +89,8 @@
 
 fun comb th1 th2 =
   let
-    val t1 = Thm.dest_arg (Thm.cconcl_of th1)
-    val t2 = Thm.dest_arg (Thm.cconcl_of th2)
+    val t1 = HOLogic.dest_judgment (Thm.cconcl_of th1)
+    val t2 = HOLogic.dest_judgment (Thm.cconcl_of th2)
     val (f, g) = Thm.dest_binop t1
     val (x, y) = Thm.dest_binop t2
     val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f)
@@ -102,8 +102,8 @@
 
 fun trans th1 th2 =
   let
-    val t1 = Thm.dest_arg (Thm.cconcl_of th1)
-    val t2 = Thm.dest_arg (Thm.cconcl_of th2)
+    val t1 = HOLogic.dest_judgment (Thm.cconcl_of th1)
+    val t2 = HOLogic.dest_judgment (Thm.cconcl_of th2)
     val (r, s) = Thm.dest_binop t1
     val t = Thm.dest_arg t2
     val ty = Thm.ctyp_of_cterm r
@@ -121,7 +121,7 @@
     val th2a = implies_elim_all th2
     val th1b = Thm.implies_intr th2c th1a
     val th2b = Thm.implies_intr th1c th2a
-    val i = Thm.instantiate' [] [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
+    val i = Thm.instantiate' [] [SOME (HOLogic.dest_judgment th1c), SOME (HOLogic.dest_judgment th2c)] @{thm iffI}
     val i1 = Thm.implies_elim i (Thm.assume_cterm (Thm.cprop_of th2b))
     val i2 = Thm.implies_elim i1 th1b
     val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2
@@ -132,7 +132,7 @@
 
 fun conj1 th =
   let
-    val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
+    val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th))
     val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1}
   in
     meta_mp i th
@@ -140,7 +140,7 @@
 
 fun conj2 th =
   let
-    val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th))
+    val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th))
     val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2}
   in
     meta_mp i th
@@ -153,7 +153,7 @@
 fun abs x th =
   let
     val th1 = implies_elim_all th
-    val (tl, tr) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1))
+    val (tl, tr) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th1))
     val (f, g) = (Thm.lambda x tl, Thm.lambda x tr)
     val (al, ar) = (Thm.apply f x, Thm.apply g x)
     val bl = beta al
@@ -250,7 +250,7 @@
 fun typedef_hollight th =
   let
     val ((rep, abs), P) =
-      Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
+      Thm.dest_comb (HOLogic.dest_judgment (Thm.cprop_of th))
       |>> (Thm.dest_comb #>> Thm.dest_arg)
       ||> Thm.dest_arg
     val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
@@ -285,7 +285,7 @@
     val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
     val th = freezeT thy' (#type_definition (#2 typedef_info))
     val (rep, abs) =
-      Thm.dest_comb (#1 (Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)))) |>> Thm.dest_arg
+      Thm.dest_comb (#1 (Thm.dest_comb (HOLogic.dest_judgment (Thm.cprop_of th)))) |>> Thm.dest_arg
     val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep)
     val typedef_th = typedef_hol2hollight A B rep abs cP (Thm.free ("a", aty)) (Thm.free ("r", ctT))
   in