src/HOL/Tools/datatype_realizer.ML

--- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 29 10:37:09 2007 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 29 16:13:41 2007 +0100
@@ -217,7 +217,7 @@
   end;
 
 fun add_dt_realizers names thy =
-  if !proofs < 2 then thy
+  if ! Proofterm.proofs < 2 then thy
   else let
     val _ = message "Adding realizers for induction and case analysis ..."
     val infos = map (DatatypePackage.the_datatype thy) names;