src/Pure/theory.ML

     val (lhs_const, rhs) = Sign.cert_def pp tm;
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in
     defs |> Defs.define (Sign.the_const_type thy)
-      name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
+      ((true, Context.theory_name thy), name) (prep_const thy lhs_const)
+      (map (prep_const thy) rhs_consts)
   end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
     Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
 

   let
     fun const_of (Const const) = const
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
     fun specify (c, T) =
-      Defs.define (Sign.the_const_type thy) (c ^ " axiom") (prep_const thy (c, T)) [];
+      Defs.define (Sign.the_const_type thy) ((false, Context.theory_name thy), c ^ " axiom") (prep_const thy (c, T)) [];
     val finalize = specify o check_overloading thy overloaded o
       const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
   in thy |> map_defs (fold finalize args) end;
 
 in