Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/cnf.ML
changeset 81954 6f2bcdfa9a19
parent 80639 3322b6ae6b19
child 81955 33616e13e172 
--- a/src/HOL/Tools/cnf.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/cnf.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -106,7 +106,7 @@
     (* becomes "[..., A1, ..., An] |- B"                                   *)
     fun prems_to_hyps thm =
       fold (fn cprem => fn thm' =>
-        Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
+        Thm.implies_elim thm' (Thm.assume cprem)) (Thm.cprems_of thm) thm
   in
     (* [...] |- ~(x1 | ... | xn) ==> False *)
     (@{thm cnf.clause2raw_notE} OF [clause])
isabelle