Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust: proper Proofterm.get_proofs_level with bound check;
authorwenzelm
Sat, 09 Dec 2023 21:15:12 +0100
changeset 79223 78d032205af4
parent 79222 86a9a7668f5e
child 79224 936ad4627a74
more robust: proper Proofterm.get_proofs_level with bound check;
src/HOL/Tools/datatype_realizer.ML file | annotate | diff | comparison | revisions
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_realizer.ML	Sat Dec 09 20:50:21 2023 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Sat Dec 09 21:15:12 2023 +0100
@@ -227,7 +227,7 @@
   end;
 
 fun add_dt_realizers config names thy =
-  if not (Proofterm.proof_enabled (! Proofterm.proofs)) then thy
+  if not (Proofterm.proof_enabled (Proofterm.get_proofs_level ())) then thy
   else
     let
       val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
--- a/src/Pure/proofterm.ML	Sat Dec 09 20:50:21 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 09 21:15:12 2023 +0100
@@ -501,7 +501,7 @@
   end;
 
 fun any_proofs_enabled () =
-  let val proofs = ! proofs
+  let val proofs = get_proofs_level ()
   in zproof_enabled proofs orelse proof_enabled proofs end;
 
 fun atomic_proof prf =
isabelle