diff -r 39ccdbbed539 -r 5727bcc3c47c src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -38,8 +38,8 @@
   val dest_theory: theory -> spec_rule list
   val retrieve: Proof.context -> term -> spec_rule list
   val retrieve_global: theory -> term -> spec_rule list
-  val add: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory
-  val add_global: string -> rough_classification -> term list -> thm list -> theory -> theory
+  val add: binding -> rough_classification -> term list -> thm list -> local_theory -> local_theory
+  val add_global: binding -> rough_classification -> term list -> thm list -> theory -> theory
 end;
 
 structure Spec_Rules: SPEC_RULES =
@@ -158,7 +158,7 @@
 
 (* add *)
 
-fun add name rough_classification terms rules lthy =
+fun add b rough_classification terms rules lthy =
   let
     val pos = Position.thread_data ();
     val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
@@ -166,6 +166,7 @@
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => fn context =>
         let
+          val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b);
           val (terms', rules') =
             map (Thm.transfer (Context.theory_of context)) thms0
             |> Morphism.fact phi
@@ -179,9 +180,12 @@
         end)
   end;
 
-fun add_global name rough_classification terms rules =
-  (Context.theory_map o Rules.map o Item_Net.update)
-    {pos = Position.thread_data (), name = name, rough_classification = rough_classification,
-      terms = terms, rules = map Thm.trim_context rules};
+fun add_global b rough_classification terms rules thy =
+  thy |> (Context.theory_map o Rules.map o Item_Net.update)
+   {pos = Position.thread_data (),
+    name = Sign.full_name thy b,
+    rough_classification = rough_classification,
+    terms = terms,
+    rules = map Thm.trim_context rules};
 
 end;