diff -r f6d9e0e0b153 -r 1de908189869 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/type.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -509,10 +509,10 @@
 fun add_class pp naming (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
-      val c' = NameSpace.full naming c;
+      val c' = NameSpace.full_name naming (Binding.name c);
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
-      val space' = space |> NameSpace.declare naming c';
+      val space' = space |> NameSpace.declare_base naming c';
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
@@ -568,8 +568,8 @@
 fun new_decl naming tags (c, decl) (space, types) =
   let
     val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val c' = NameSpace.full naming c;
-    val space' = NameSpace.declare naming c' space;
+    val c' = NameSpace.full_name naming (Binding.name c);
+    val space' = NameSpace.declare_base naming c' space;
     val types' =
       (case Symtab.lookup types c' of
         SOME ((decl', _), _) => err_in_decls c' decl decl'