--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 15:52:30 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 16:14:51 2009 +0200
@@ -308,7 +308,7 @@
val ((dummies, some_dt_names), thy2) =
thy1
|> add_dummies (Datatype.add_datatype
- { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
+ { strict = 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;