--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Tue Jun 16 16:37:07 2009 +0200
@@ -7,7 +7,7 @@
signature DATATYPE_REALIZER =
sig
- val add_dt_realizers: string list -> theory -> theory
+ val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
val setup: theory -> theory
end;
@@ -213,10 +213,10 @@
(exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
end;
-fun add_dt_realizers names thy =
+fun add_dt_realizers config names thy =
if ! Proofterm.proofs < 2 then thy
else let
- val _ = message "Adding realizers for induction and case analysis ..."
+ val _ = message config "Adding realizers for induction and case analysis ..."
val infos = map (DatatypePackage.the_datatype thy) names;
val info :: _ = infos;
in