1.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4               ||> add_recursor
     1.5               ||> Sign.parent_path
     1.6  
     1.7 -  val intr_names = map #2 (List.concat con_ty_lists);
     1.8 +  val intr_names = map (Name.binding o #2) (List.concat con_ty_lists);
     1.9    val (thy1, ind_result) =
    1.10      thy0 |> Ind_Package.add_inductive_i
    1.11        false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))