src/Pure/Isar/object_logic.ML

 (* typedecl *)
 
 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;
     val T = Type (name, map (fn v => TFree (v, [])) vs);
   in

 (* add judgment *)
 
 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')
     |> map_data (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"