proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";

--- a/src/Pure/Proof/extraction.ML	Sat Nov 30 16:46:34 2019 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Dec 01 15:38:36 2019 +0100
@@ -824,7 +824,8 @@
            [((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 [head] [def_thm]
+           Spec_Rules.add_global const_name Spec_Rules.equational
+             [Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
            #> Code.declare_default_eqns_global [(def_thm, true)])
       end;