# HG changeset patch
# User wenzelm
# Date 1575211116 -3600
# Node ID 20dce31fe7f40b0ace832f5c4a8e7ea18cf1def3
# Parent  95e12ecdcb5f558ac78b8bada7b4d399e60ce086
proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";

diff -r 95e12ecdcb5f -r 20dce31fe7f4 src/Pure/Proof/extraction.ML
--- 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;