src/HOL/Tools/datatype_realizer.ML
changeset 25223 7463251e7273
parent 24712 64ed05609568
child 26359 6d437bde2f1d
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 29 10:37:09 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 29 16:13:41 2007 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4    end;
     1.5  
     1.6  fun add_dt_realizers names thy =
     1.7 -  if !proofs < 2 then thy
     1.8 +  if ! Proofterm.proofs < 2 then thy
     1.9    else let
    1.10      val _ = message "Adding realizers for induction and case analysis ..."
    1.11      val infos = map (DatatypePackage.the_datatype thy) names;