--- 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