# HG changeset patch
# User wenzelm
# Date 1575290042 -3600
# Node ID 39ccdbbed539312edf16025db987a163986ebcbf
# Parent  475510f1a280b82016d8eae79c94deaebee7e833
more informative spec rules;

diff -r 475510f1a280 -r 39ccdbbed539 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Dec 02 13:33:45 2019 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Dec 02 13:34:02 2019 +0100
@@ -216,6 +216,11 @@
     val specs =
       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));
+
+
     (*consts*)
     val (consts, consts_thy) = thy
       |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
@@ -229,7 +234,7 @@
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
       |> Named_Target.theory_init
-      |> Spec_Rules.add "" Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms)
+      |> Spec_Rules.add spec_name Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms)
       |> Local_Theory.notes axioms;
 
   in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;