Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Fri, 15 Oct 2021 21:59:46 +0200
changeset 74529 a1aa42743d7d
parent 74528 ce2c7037e509
child 74530 823ccd84b879
tuned;
src/HOL/Library/simps_case_conv.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle