diff -r 954321008785 -r 10e1a6ea8df9 src/HOL/Tools/inductive_realizer.ML
--- 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;