# HG changeset patch
# User haftmann
# Date 1514839327 0
# Node ID eabcd2e2bc9bb10594c4f6bf973c7dd30af8b719
# Parent  5ca7bb565ea29042082bb11d7fa472595891d595
tuned

diff -r 5ca7bb565ea2 -r eabcd2e2bc9b src/HOL/Tools/simpdata.ML
--- 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