dropped ancient flat_names option
authorhaftmann
Tue Jul 21 16:14:51 2009 +0200 (2009-07-21)
changeset 3212510e1a6ea8df9
parent 32124 954321008785
child 32126 a5042f260440
dropped ancient flat_names option
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 21 15:52:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 21 16:14:51 2009 +0200
     1.3 @@ -308,7 +308,7 @@
     1.4      val ((dummies, some_dt_names), thy2) =
     1.5        thy1
     1.6        |> add_dummies (Datatype.add_datatype
     1.7 -           { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
     1.8 +           { strict = false, quiet = false } (map (Binding.name_of o #2) dts))
     1.9             (map (pair false) dts) []
    1.10        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.11        ||> Extraction.add_realizes_eqns_i rlz_eqs;