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 ...";