merged

--- a/src/Doc/Sledgehammer/document/root.tex	Wed Sep 22 12:03:59 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Sep 22 14:32:20 2021 +0200
@@ -159,9 +159,7 @@
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package, it should
 already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
-and Z3, ready to use. To use Vampire, you must confirm that you are a
-noncommercial user, as indicated by the message that is displayed when
-Sledgehammer is invoked the first time.
+and Z3, ready to use.
 
 \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
 SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract the

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 12:03:59 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 14:32:20 2021 +0200
@@ -45,7 +45,6 @@
   val spass_H2NuVS0 : string
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
-  val is_vampire_noncommercial_license_accepted : unit -> bool option
   val isabelle_scala_function: string list * string list
   val remote_atp : string -> string -> string list -> (string * string) list ->
     (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
@@ -319,7 +318,7 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     ["--clausifier \"$OLD_VAMPIRE_HOME\"/vampire " ^
+     ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
       "--clausifier_options \"--mode clausify\" " ^
       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
@@ -452,31 +451,6 @@
 
 (* Vampire *)
 
-fun is_vampire_noncommercial_license_accepted () =
-  let
-    val flag = Options.default_string \<^system_option>\<open>vampire_noncommercial\<close>
-      |> String.map Char.toLower
-  in
-    if flag = "yes" then
-      SOME true
-    else if flag = "no" then
-      SOME false
-    else
-      NONE
-  end
-
-fun check_vampire_noncommercial () =
-  (case is_vampire_noncommercial_license_accepted () of
-    SOME true => ()
-  | SOME false =>
-    error (Pretty.string_of (Pretty.para
-      "The Vampire prover may be used only for noncommercial applications"))
-  | NONE =>
-    error (Pretty.string_of (Pretty.para
-      "The Vampire prover is not activated; to activate it, set the Isabelle system option \
-      \\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \
-      \/ Isabelle / General)")))
-
 val vampire_basic_options =
   "--proof tptp --output_axiom_names on" ^
   (if ML_System.platform_is_windows
@@ -488,14 +462,13 @@
 
 val vampire_config : atp_config =
   let
-    val format = TFF (Without_FOOL, Monomorphic)
+    val format = TFF (With_FOOL, Monomorphic)
   in
-    {exec = (["OLD_VAMPIRE_HOME"], ["vampire"]),
+    {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
-       (check_vampire_noncommercial ();
-        [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+       [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
          " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
-         |> sos = sosN ? prefix "--sos on "]),
+         |> sos = sosN ? prefix "--sos on "],
      proof_delims =
        [("=========== Refutation ==========",
          "======= End of refutation =======")] @

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Sep 22 12:03:59 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Sep 22 14:32:20 2021 +0200
@@ -177,9 +177,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [cvc4N] @
-  (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @
-  [z3N, eN, spassN, veritN]
+  [cvc4N, vampireN, z3N, eN, spassN, veritN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))

--- a/src/HOL/Tools/etc/options	Wed Sep 22 12:03:59 2021 +0200
+++ b/src/HOL/Tools/etc/options	Wed Sep 22 14:32:20 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"