diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -1034,7 +1034,7 @@
     val process =
       rewrite_rule ctxt (Named_Theorems.get ctxt @{named_theorems code_pred_simp})
     fun process_False intro_t =
-      if member (=) (Logic.strip_imp_prems intro_t) @{prop "False"}
+      if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
       then NONE else SOME intro_t
     fun process_True intro_t =
       map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t