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
authorhaftmann
Mon, 01 Jan 2018 20:42:07 +0000
changeset 67329 eabcd2e2bc9b
parent 67328 5ca7bb565ea2
child 67330 2505cabfc515
tuned
src/HOL/Tools/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/simpdata.ML	Mon Jan 01 20:42:06 2018 +0000
+++ b/src/HOL/Tools/simpdata.ML	Mon Jan 01 20:42:07 2018 +0000
@@ -58,7 +58,7 @@
 
 fun lift_meta_eq_to_obj_eq ctxt i st =
   let
-    fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
+    fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ _ $ P) = 1 + count_imp P
       | count_imp _ = 0;
     val j = count_imp (Logic.strip_assums_concl (Thm.term_of (Thm.cprem_of st i)))
   in
isabelle