--- 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