src/HOL/Tools/Datatype/datatype_realizer.ML

--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 03 18:57:42 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 03 19:21:12 2011 +0100
@@ -214,7 +214,7 @@
   end;
 
 fun add_dt_realizers config names thy =
-  if ! Proofterm.proofs < 2 then thy
+  if not (Proofterm.proofs_enabled ()) then thy
   else
     let
       val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";