equal
deleted
inserted
replaced
938 | do_conceal_lambdas _ t = t |
938 | do_conceal_lambdas _ t = t |
939 val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas) |
939 val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas) |
940 |
940 |
941 fun do_introduce_combinators ctxt Ts t = |
941 fun do_introduce_combinators ctxt Ts t = |
942 let val thy = Proof_Context.theory_of ctxt in |
942 let val thy = Proof_Context.theory_of ctxt in |
943 t |> not (Meson.is_fol_term thy t) |
943 t |> conceal_bounds Ts |
944 ? (conceal_bounds Ts |
944 |> cterm_of thy |
945 #> cterm_of thy |
945 |> Meson_Clausify.introduce_combinators_in_cterm |
946 #> Meson_Clausify.introduce_combinators_in_cterm |
946 |> prop_of |> Logic.dest_equals |> snd |
947 #> prop_of #> Logic.dest_equals #> snd |
947 |> reveal_bounds Ts |
948 #> reveal_bounds Ts) |
|
949 end |
948 end |
950 (* A type variable of sort "{}" will make abstraction fail. *) |
949 (* A type variable of sort "{}" will make abstraction fail. *) |
951 handle THM _ => t |> do_conceal_lambdas Ts |
950 handle THM _ => t |> do_conceal_lambdas Ts |
952 val introduce_combinators = simple_translate_lambdas do_introduce_combinators |
951 val introduce_combinators = simple_translate_lambdas do_introduce_combinators |
953 |
952 |