--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jan 10 15:25:09 2018 +0100
@@ -1036,7 +1036,7 @@
#> raw_mangled_const_name generic_mangled_type_name
val parse_mangled_ident =
- Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
+ Scan.many1 (not o member (=) ["(", ")", ","]) >> implode
fun parse_mangled_type x =
(parse_mangled_ident
@@ -1796,7 +1796,7 @@
else if lam_trans = combs_or_liftingN then
lift_lams_part_1 ctxt type_enc
##> map (fn t => (case head_of (strip_qnt_body @{const_name All} t) of
- @{term "op = ::bool => bool => bool"} => t
+ @{term "(=) ::bool => bool => bool"} => t
| _ => introduce_combinators ctxt (intentionalize_def t)))
#> lift_lams_part_2 ctxt
else if lam_trans = keep_lamsN then