--- 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;