src/HOL/Nominal/nominal_inductive2.ML
changeset 67405 e9ab4ad7bd15
parent 67399 eab6ce8368fa
child 67522 9e712280cc37
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -49,7 +49,7 @@
     proc = fn _ => fn _ => fn ct =>
       (case Thm.term_of ct of
         Const (@{const_name Nominal.perm}, _) $ _ $ t =>
-          if member (=) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
        | _ => NONE)};