src/Pure/type.ML

--- a/src/Pure/type.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/type.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -509,10 +509,9 @@
 fun add_class pp naming (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
-      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_base naming c';
+      val (c', space') = space |> NameSpace.declare naming (Binding.name c);
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
@@ -568,8 +567,7 @@
 fun new_decl naming tags (c, decl) (space, types) =
   let
     val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val c' = NameSpace.full_name naming (Binding.name c);
-    val space' = NameSpace.declare_base naming c' space;
+    val (c', space') = NameSpace.declare naming (Binding.name c) space;
     val types' =
       (case Symtab.lookup types c' of
         SOME ((decl', _), _) => err_in_decls c' decl decl'