# HG changeset patch
# User nipkow
# Date 1587676340 -7200
# Node ID 54d4bfa48025fe6f9f1707da0b4463da519520b3
# Parent  ac28714b74782108e1cd241dc57644b110c3ee70# Parent  641f4c8ffec8be0d347099b55aa9c870bfdbcc41
merged

diff -r 641f4c8ffec8 -r 54d4bfa48025 etc/settings
--- a/etc/settings	Thu Apr 23 23:08:29 2020 +0200
+++ b/etc/settings	Thu Apr 23 23:12:20 2020 +0200
@@ -14,9 +14,9 @@
 
 ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2"
 
-ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss16m"
+ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
 
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx2560m -J-Xss16m"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
diff -r 641f4c8ffec8 -r 54d4bfa48025 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Thu Apr 23 23:08:29 2020 +0200
+++ b/src/HOL/ATP.thy	Thu Apr 23 23:12:20 2020 +0200
@@ -137,6 +137,5 @@
 ML_file \<open>Tools/monomorph.ML\<close>
 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
-ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 
 end
diff -r 641f4c8ffec8 -r 54d4bfa48025 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Apr 23 23:08:29 2020 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Apr 23 23:12:20 2020 +0200
@@ -16,6 +16,7 @@
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   by (erule contrapos_nn) (rule arg_cong)
 
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
diff -r 641f4c8ffec8 -r 54d4bfa48025 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 23 23:08:29 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 23 23:12:20 2020 +0200
@@ -453,7 +453,7 @@
       (InternalError, "Please report this error")] @
       known_perl_failures,
    prem_role = Conjecture,
-   best_slices = fn ctxt =>
+   best_slices = fn _ =>
      (* FUDGE *)
      [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
       (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
@@ -499,7 +499,7 @@
 val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
 
 val vampire_full_proof_options =
-  " --forced_options equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
+  " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
 val remote_vampire_command =
   "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
diff -r 641f4c8ffec8 -r 54d4bfa48025 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Apr 23 23:08:29 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Apr 23 23:12:20 2020 +0200
@@ -85,7 +85,7 @@
              fun mk_step fact_names meths =
                Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
            in
-             (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
+             (case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of
                (res as (meth, Played time)) :: _ =>
                (* if a fact is needed by an ATP, it will be needed by "metis" *)
                if not minimize orelse is_metis_method meth then
diff -r 641f4c8ffec8 -r 54d4bfa48025 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Apr 23 23:08:29 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Apr 23 23:12:20 2020 +0200
@@ -51,23 +51,21 @@
   @volatile private var _settings: Option[Map[String, String]] = None
   @volatile private var _services: Option[List[Service]] = None
 
-  private def uninitialized: Boolean = _services.isEmpty   // unsynchronized check
-
   def settings(): Map[String, String] =
   {
-    if (uninitialized) init()
+    if (_settings.isEmpty) init()  // unsynchronized check
     _settings.get
   }
 
   def services(): List[Service] =
   {
-    if (uninitialized) init()
+    if (_services.isEmpty) init()  // unsynchronized check
     _services.get
   }
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
   {
-    if (uninitialized) {
+    if (_settings.isEmpty || _services.isEmpty) {
       val isabelle_root1 =
         bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
 
diff -r 641f4c8ffec8 -r 54d4bfa48025 src/Tools/jEdit/etc/settings
--- a/src/Tools/jEdit/etc/settings	Thu Apr 23 23:08:29 2020 +0200
+++ b/src/Tools/jEdit/etc/settings	Thu Apr 23 23:12:20 2020 +0200
@@ -5,7 +5,7 @@
 
 JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
 
-JEDIT_JAVA_OPTIONS="-Xms512m -Xmx2560m -Xss8m"
+JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
 JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
 
 ISABELLE_JEDIT_OPTIONS=""