src/HOL/Tools/datatype_prop.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
     1.1 --- a/src/HOL/Tools/datatype_prop.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_prop.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4    let
     1.5      fun type_name (TFree (name, _)) = implode (tl (explode name))
     1.6        | type_name (Type (name, _)) = 
     1.7 -          let val name' = NameSpace.base_name name
     1.8 +          let val name' = Long_Name.base_name name
     1.9            in if Syntax.is_identifier name' then name' else "x" end;
    1.10    in indexify_names (map type_name Ts) end;
    1.11