changeset 67405 | e9ab4ad7bd15 |
parent 67399 | eab6ce8368fa |
child 69593 | 3dda49e08b9d |
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Thu Jan 11 12:32:07 2018 +0100 +++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Thu Jan 11 13:48:17 2018 +0100 @@ -530,7 +530,7 @@ val def = specialize_type thy x def0; val lhs = lhs_of_equation def; in - if exists_Const (curry (=) x) lhs then def else raise Fail "cannot specialize" + if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize" end; fun definition_of thy (x as (s, _)) =