src/Pure/Isar/specification.ML

     val close = Logic.close_prop (map #2 fixes @ frees) prems;
     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));
+      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;

     val name = Thm.def_binding_optional b a;
     val ((lhs, (_, raw_th)), lthy2) = lthy
       |> 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], [])])];
 
     val lthy5 = lthy4