--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 19 13:58:12 2017 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 20 12:22:36 2017 +0100
@@ -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 "op = ::bool => bool => bool"} => t
| _ => introduce_combinators ctxt (intentionalize_def t)))
#> lift_lams_part_2 ctxt
else if lam_trans = keep_lamsN then