src/HOL/Tools/Datatype/datatype.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 33959 2afc55e8ed27
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Nov 24 17:28:44 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 09:13:46 2009 +0100
     1.3 @@ -328,7 +328,7 @@
     1.4         ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
     1.5      val unnamed_rules = map (fn induct =>
     1.6        ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
     1.7 -        ((uncurry drop) (length dt_names, inducts));
     1.8 +        (drop (length dt_names) inducts);
     1.9    in
    1.10      thy9
    1.11      |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),