diff -r f6d9e0e0b153 -r 1de908189869 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/Isar/object_logic.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -89,7 +89,7 @@
 fun typedecl (raw_name, vs, mx) thy =
   let
     val base_sort = get_base_sort thy;
-    val name = Sign.full_name thy (Syntax.type_name raw_name mx);
+    val name = Sign.full_bname thy (Syntax.type_name raw_name mx);
     val _ = has_duplicates (op =) vs andalso
       error ("Duplicate parameters in type declaration: " ^ quote name);
     val n = length vs;
@@ -107,7 +107,7 @@
 local
 
 fun gen_add_judgment add_consts (bname, T, mx) thy =
-  let val c = Sign.full_name thy (Syntax.const_name bname mx) in
+  let val c = Sign.full_bname thy (Syntax.const_name bname mx) in
     thy
     |> add_consts [(bname, T, mx)]
     |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')