src/HOL/Tools/datatype_prop.ML

--- a/src/HOL/Tools/datatype_prop.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -47,7 +47,7 @@
   let
     fun type_name (TFree (name, _)) = implode (tl (explode name))
       | type_name (Type (name, _)) = 
-          let val name' = Sign.base_name name
+          let val name' = NameSpace.base_name name
           in if Syntax.is_identifier name' then name' else "x" end;
   in indexify_names (map type_name Ts) end;