author | wenzelm |
Fri, 15 Oct 2021 11:42:36 +0200 | |
changeset 74520 | 02d90c4360de |
parent 74519 | fc65e39ca170 |
child 74521 | 854537af4ce8 |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 01:44:52 2021 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 15 11:42:36 2021 +0200 @@ -135,7 +135,7 @@ | _ => raise Fail "abstract: Bad term" end; -(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) +(* Traverse a theorem, replacing lambda-abstractions with combinators. *) fun introduce_combinators_in_cterm ctxt ct = if is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct