tuned op's
authornipkow
Wed Dec 20 12:22:36 2017 +0100 (17 months ago)
changeset 672287c7b76695c90
parent 67226 ec32cdaab97b
child 67229 4ecf0ef70efb
tuned op's
src/HOL/Tools/ATP/atp_problem_generate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 19 13:58:12 2017 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Dec 20 12:22:36 2017 +0100
     1.3 @@ -1796,7 +1796,7 @@
     1.4    else if lam_trans = combs_or_liftingN then
     1.5      lift_lams_part_1 ctxt type_enc
     1.6      ##> map (fn t => (case head_of (strip_qnt_body @{const_name All} t) of
     1.7 -                       @{term "op =::bool => bool => bool"} => t
     1.8 +                       @{term "op = ::bool => bool => bool"} => t
     1.9                       | _ => introduce_combinators ctxt (intentionalize_def t)))
    1.10      #> lift_lams_part_2 ctxt
    1.11    else if lam_trans = keep_lamsN then