src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Dec 07 08:14:40 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Dec 08 15:21:18 2016 +0100
@@ -152,6 +152,7 @@
              THEN TRY (
                 let
                   val prems' = maps dest_conjunct_prem (take nargs prems)
+                    |> filter is_equationlike
                 in
                   rewrite_goal_tac ctxt'
                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1