src/HOL/Nominal/nominal_inductive2.ML
changeset 67399 eab6ce8368fa
parent 65411 3c628937899d
child 67405 e9ab4ad7bd15
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jan 10 15:25:09 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 (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+          if member (=) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
        | _ => NONE)};