# HG changeset patch
# User wenzelm
# Date 1634327986 -7200
# Node ID a1aa42743d7dab2985a5ed50d1742ddcdffc4d5a
# Parent  ce2c7037e509c628cb69658b87cad8d08b136e9f
tuned;

diff -r ce2c7037e509 -r a1aa42743d7d src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Fri Oct 15 21:25:47 2021 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Fri Oct 15 21:59:46 2021 +0200
@@ -64,8 +64,7 @@
   let
     val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
     val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
-    fun dest_alls (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = dest_alls t
-      | dest_alls t = t
+    val dest_alls = Term.strip_qnt_body \<^const_name>\<open>All\<close>
   in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
   handle TERM _ => false