src/HOL/Tools/Datatype/datatype_aux.ML
changeset 33317 b4534348b8fd
parent 33244 db230399f890
child 33338 de76079f973a
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  
     1.5  fun name_of_typ (Type (s, Ts)) =
     1.6        let val s' = Long_Name.base_name s
     1.7 -      in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
     1.8 +      in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
     1.9          [if Syntax.is_identifier s' then s' else "x"])
    1.10        end
    1.11    | name_of_typ _ = "";
    1.12 @@ -272,7 +272,7 @@
    1.13  
    1.14  fun get_arities descr = fold (fn (_, (_, _, constrs)) =>
    1.15    fold (fn (_, cargs) => fold (insert op =) (map (length o fst o strip_dtyp)
    1.16 -    (List.filter is_rec_type cargs))) constrs) descr [];
    1.17 +    (filter is_rec_type cargs))) constrs) descr [];
    1.18  
    1.19  (* interpret construction of datatype *)
    1.20