proper spec_rule name via naming/binding/Morphism.binding;

--- a/src/HOL/Library/old_recdef.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -2842,7 +2842,7 @@
       |> Global_Theory.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global name Spec_Rules.equational_recdef [lhs] (flat rules)
+      ||> Spec_Rules.add_global (Binding.name bname) Spec_Rules.equational_recdef [lhs] (flat rules)
       ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy3 =

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -1414,10 +1414,13 @@
           |> massage_simple_notes fp_b_name;
 
         val (noted, lthy') = lthy
-          |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) map_thms)
+          |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+                (`(single o lhs_head_of o hd) map_thms)
           |> fp = Least_FP ?
-              uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) rel_code_thms)
-          |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) set0_thms)
+              uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+                (`(single o lhs_head_of o hd) rel_code_thms)
+          |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+                (`(single o lhs_head_of o hd) set0_thms)
           |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
           |> Local_Theory.notes (anonymous_notes @ notes);
 
@@ -2689,7 +2692,7 @@
           |> massage_multi_notes fp_b_names fpTs;
       in
         lthy
-        |> Spec_Rules.add "" Spec_Rules.equational recs (flat rec_thmss)
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational recs (flat rec_thmss)
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
         |> Local_Theory.notes (common_notes @ notes)
         (* for "datatype_realizer.ML": *)
@@ -2869,7 +2872,7 @@
           |> massage_multi_notes fp_b_names fpTs;
       in
         lthy
-        |> fold (Spec_Rules.add "" Spec_Rules.equational corecs)
+        |> fold (Spec_Rules.add Binding.empty Spec_Rules.equational corecs)
           [flat corec_sel_thmss, flat corec_thmss]
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
         |> Local_Theory.notes (common_notes @ notes)

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -2157,7 +2157,7 @@
         |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat ctr_thmss)
 *)
-        |> Spec_Rules.add "" Spec_Rules.equational [fun_lhs] [code_thm]
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational [fun_lhs] [code_thm]
         |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -1533,9 +1533,10 @@
         val fun_ts0 = map fst def_infos;
       in
         lthy
-        |> Spec_Rules.add "" (Spec_Rules.equational_primcorec primcorec_types) fun_ts0 (flat sel_thmss)
-        |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat ctr_thmss)
-        |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat code_thmss)
+        |> Spec_Rules.add Binding.empty (Spec_Rules.equational_primcorec primcorec_types)
+            fun_ts0 (flat sel_thmss)
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat ctr_thmss)
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat code_thmss)
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
         |> snd

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -637,7 +637,7 @@
     val transfer = exists (can (fn Transfer_Option => ())) opts;
 
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
-    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
+    val spec_name = Binding.conglomerate (map (#1 o #1) fixes);
 
     val mk_notes =
       flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -373,8 +373,9 @@
 
       val (noted, lthy3) =
         lthy2
-        |> Spec_Rules.add "" Spec_Rules.equational size_consts size_simps
-        |> Spec_Rules.add "" Spec_Rules.equational overloaded_size_consts overloaded_size_simps
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational size_consts size_simps
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational
+            overloaded_size_consts overloaded_size_simps
         |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
           (*Ideally, this would be issued only if the "code" plugin is enabled.*)
         |> Local_Theory.notes notes;

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -1111,10 +1111,10 @@
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
 
         val (noted, lthy') = lthy
-          |> Spec_Rules.add "" Spec_Rules.equational [casex] case_thms
-          |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
+          |> Spec_Rules.add Binding.empty Spec_Rules.equational [casex] case_thms
+          |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
             (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
-          |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
+          |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
             (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
           |> Local_Theory.declaration {syntax = false, pervasive = true}
             (fn phi => Case_Translation.register

--- a/src/HOL/Tools/Function/function.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -211,7 +211,7 @@
              lthy2
              |> Local_Theory.declaration {syntax = false, pervasive = false}
                (fn phi => add_function_data (transform_function_data phi info'))
-             |> Spec_Rules.add "" Spec_Rules.equational_recdef fs tsimps)
+             |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps)
           end)
       end
   in

--- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -302,7 +302,7 @@
     val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
   in
     lthy''
-    |> Spec_Rules.add "" Spec_Rules.equational_recdef [f] [rec_rule']
+    |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef [f] [rec_rule']
     |> note_qualified ("simps", [rec_rule'])
     |> note_qualified ("mono", [mono_thm])
     |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))

--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -278,7 +278,7 @@
 fun gen_primrec prep_spec int raw_fixes raw_spec lthy =
   let
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
-    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
+    val spec_name = Binding.conglomerate (map (#1 o #1) fixes);
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
       (Binding.qualify false prefix b, attrs)) spec;
     fun simp_attr_binding prefix =

--- a/src/HOL/Tools/inductive.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -71,7 +71,7 @@
     term list -> (Attrib.binding * term) list -> thm list ->
     term list -> (binding * mixfix) list ->
     local_theory -> result * local_theory
-  val declare_rules: binding -> bool -> bool -> string -> string list -> term list ->
+  val declare_rules: binding -> bool -> bool -> binding -> string list -> term list ->
     thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
     thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
   val add_ind_def: add_ind_def
@@ -1099,7 +1099,7 @@
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
-    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map #1 cnames_syn));
+    val spec_name = Binding.conglomerate (map #1 cnames_syn);
     val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule lthy cs params) intros));

--- a/src/HOL/Tools/inductive_set.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -503,7 +503,7 @@
     val rec_name =
       if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name;
     val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
-    val spec_name = Local_Theory.full_name lthy3 (Binding.conglomerate (map #1 cnames_syn));
+    val spec_name = Binding.conglomerate (map #1 cnames_syn);
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     val (intrs', elims', eqs', induct, inducts, lthy4) =

--- a/src/HOL/Tools/record.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/record.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -1814,7 +1814,7 @@
 
 fun add_spec_rule rule =
   let val head = head_of (lhs_of_equation (Thm.prop_of rule))
-  in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end;
+  in Spec_Rules.add_global Binding.empty Spec_Rules.equational [head] [rule] end;
 
 (* definition *)
 

--- 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;

--- a/src/Pure/Isar/specification.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -217,8 +217,7 @@
       map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
 
     val spec_name =
-      Sign.full_name thy
-        (Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls));
+      Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls);
 
 
     (*consts*)
@@ -270,7 +269,7 @@
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
-    val lthy3 = lthy2 |> Spec_Rules.add const_name Spec_Rules.equational [lhs] [th];
+    val lthy3 = lthy2 |> Spec_Rules.add b Spec_Rules.equational [lhs] [th];
 
     val ([(def_name, [th'])], lthy4) = lthy3
       |> Local_Theory.notes [((name, atts), [([th], [])])];

--- a/src/Pure/Proof/extraction.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -816,7 +816,6 @@
         val fu = Type.legacy_freeze u;
         val head = head_of (strip_abs_body fu);
         val b = Binding.qualified_name (extr_name s vs);
-        val const_name = Sign.full_name thy b;
       in
         thy
         |> Sign.add_consts [(b, fastype_of ft, NoSyn)]
@@ -824,7 +823,7 @@
            [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
              Logic.mk_equals (head, ft)), [])]
         |-> (fn [def_thm] =>
-           Spec_Rules.add_global const_name Spec_Rules.equational
+           Spec_Rules.add_global b Spec_Rules.equational
              [Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
            #> Code.declare_default_eqns_global [(def_thm, true)])
       end;