--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 16 16:37:07 2009 +0200
@@ -307,8 +307,8 @@
val ((dummies, dt_info), thy2) =
thy1
- |> add_dummies
- (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
+ |> add_dummies (DatatypePackage.add_datatype
+ { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
(map (pair false) dts) []
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;