changeset 27112 | 661a74bafeb7 |
parent 26928 | ca87aff1ad2d |
child 27330 | 1af2598b5f7d |
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 10 15:31:03 2008 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 10 15:31:04 2008 +0200 @@ -312,7 +312,7 @@ val ((dummies, dt_info), thy2) = thy1 |> add_dummies - (DatatypePackage.add_datatype_i false false (map #2 dts)) + (DatatypePackage.add_datatype false false (map #2 dts)) (map (pair false) dts) [] ||> Extraction.add_typeof_eqns_i ty_eqs ||> Extraction.add_realizes_eqns_i rlz_eqs;