tuned;
authorwenzelm
Fri, 15 Oct 2021 21:59:46 +0200
changeset 74916 a1aa42743d7d
parent 74915 ce2c7037e509
child 74917 823ccd84b879
tuned;
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