diff -r 39ccdbbed539 -r 5727bcc3c47c src/Pure/Proof/extraction.ML
--- 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;