Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/goal.ML
changeset 79113 5109e4b2a292
parent 78086 5edd5b12017d 
--- a/src/Pure/goal.ML	Fri Dec 01 18:12:18 2023 +0100
+++ b/src/Pure/goal.ML	Sat Dec 02 15:42:50 2023 +0100
@@ -101,7 +101,7 @@
 
 fun skip_proofs_enabled () =
   let val skip = Options.default_bool "skip_proofs" in
-    if Proofterm.proofs_enabled () andalso skip then
+    if Proofterm.any_proofs_enabled () andalso skip then
       (warning "Proof terms enabled -- cannot skip proofs"; false)
     else skip
   end;
@@ -166,7 +166,7 @@
 
     val schematic = exists Term.is_schematic props;
     val immediate = is_none fork_pri;
-    val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
+    val future = Future.proofs_enabled 1 andalso not (Proofterm.any_proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
isabelle