# HG changeset patch
# User wenzelm
# Date 1634290956 -7200
# Node ID 02d90c4360de6b81eb323622062a81fb8763e06f
# Parent  fc65e39ca170c7d3693bf6a7889c506a86142512
spelling;

diff -r fc65e39ca170 -r 02d90c4360de src/HOL/Tools/Meson/meson_clausify.ML
--- 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