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)};