diff -r 122f8a8b718e -r b7c22754818c NEWS
--- a/NEWS	Wed Jan 08 14:51:32 2025 +0100
+++ b/NEWS	Wed Jan 08 15:00:35 2025 +0100
@@ -240,7 +240,7 @@
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
   - Added instantiations of facts using the "of" attribute
     (e.g. "assms(1)[of x]"), which can be activated using the
-    Sledgehammer option "suggest_of" (default: smart, i.e. only if
+    Sledgehammer option "instantiate" (default: smart, i.e. only if
     preplaying failed).  This uses Metis internally to infer the
     variable instantiations (see below).
   - Added extensionality (fact "ext") to some "metis (lifting)" calls.
@@ -248,7 +248,7 @@
 
 * Metis:
   - Added inference of variable instantiations, which can be activated
-    using the configuration option "metis_suggest_of" (default: false).
+    using the configuration option "metis_instantiate" (default: false).
     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").