src/Pure/Isar/spec_rules.ML

   val get: Proof.context -> spec_rule list
   val get_global: theory -> spec_rule list
   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 =
 struct
 

 val retrieve_global = retrieve_generic o Context.Theory;
 
 
 (* 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);
   in
     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
             |> chop (length terms)
             |>> map (Thm.term_of o Drule.dest_term)

             {pos = pos, name = name, rough_classification = rough_classification,
               terms = terms', rules = rules'}
         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;