# HG changeset patch
# User wenzelm
# Date 1702152912 -3600
# Node ID 78d032205af41ce627f8e9753ca20369e91f703d
# Parent  86a9a7668f5e16f3a00bda6346601d3239157f1d
more robust: proper Proofterm.get_proofs_level with bound check;

diff -r 86a9a7668f5e -r 78d032205af4 src/HOL/Tools/datatype_realizer.ML
--- 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 ...";
diff -r 86a9a7668f5e -r 78d032205af4 src/Pure/proofterm.ML
--- 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 =