src/HOL/Tools/inductive_realizer.ML
changeset 31668 a616e56a5ec8
parent 31458 b1cf26f2919b
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 16 16:36:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 16 16:37:07 2009 +0200
     1.3 @@ -307,8 +307,8 @@
     1.4  
     1.5      val ((dummies, dt_info), thy2) =
     1.6        thy1
     1.7 -      |> add_dummies
     1.8 -           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
     1.9 +      |> add_dummies (DatatypePackage.add_datatype
    1.10 +           { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    1.11             (map (pair false) dts) []
    1.12        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.13        ||> Extraction.add_realizes_eqns_i rlz_eqs;