src/Pure/Isar/theory_target.ML

 
 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
   let
     val c' = Morphism.name phi c;
     val rhs' = Morphism.term phi rhs;
-    val name' = Name.name_of c';
+    val name' = Name.name_with_prefix c';
     val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
     val arg = (name', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val class_global = Name.name_of c = Name.name_of c'
       andalso not (null (Name.prefix_of c'))
       andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
+        (fn thy => thy |> 
+          Sign.no_base_names
+          |> Sign.add_abbrev PrintMode.internal tags legacy_arg
+          ||> Sign.restore_naming thy)
         (ProofContext.add_abbrev PrintMode.internal tags arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))