diff -r d8dbe7525ff1 -r fb8ce6090437 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Wed Sep 22 12:25:09 2021 +0200
+++ b/src/HOL/Tools/etc/options	Wed Sep 22 12:41:40 2021 +0200
@@ -32,9 +32,6 @@
 public option sledgehammer_timeout : int = 30
   -- "provers will be interrupted after this time (in seconds)"
 
-public option vampire_noncommercial : string = "unknown"
-  -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
-
 public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
   -- "URL for SystemOnTPTP service"