# HG changeset patch
# User nipkow
# Date 1513768956 -3600
# Node ID 7c7b76695c9078ad9e4b9a85b9cbbff0c7bd18fb
# Parent  ec32cdaab97bf7ae19f82870d334631ad822175f
tuned op's

diff -r ec32cdaab97b -r 7c7b76695c90 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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