--- 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'