# HG changeset patch
# User haftmann
# Date 1248185691 -7200
# Node ID 10e1a6ea8df9de8b8c8808e269526ed2279440b6
# Parent  9543210087853100f55ff1f79be700a9ae210a5a
dropped ancient flat_names option

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;