# HG changeset patch
# User haftmann
# Date 1497956864 -7200
# Node ID fd3e128b174f33360b84a6239a5ecd66cdb2d71e
# Parent  4efbcc308ca017c9703df8438000dff4c22190a8
register equations stemming from extracted proofs as specification rules

diff -r 4efbcc308ca0 -r fd3e128b174f src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Jun 20 13:07:43 2017 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jun 20 13:07:44 2017 +0200
@@ -793,13 +793,16 @@
       let
         val ft = Type.legacy_freeze t;
         val fu = Type.legacy_freeze u;
+        val head = head_of (strip_abs_body fu);
       in
         thy
         |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
         |> Global_Theory.add_defs false
            [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
-             Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
-        |-> (fn [def_thm] => Code.add_eqn (Code.Equation, true) def_thm)
+             Logic.mk_equals (head, ft)), [])]
+        |-> (fn [def_thm] =>
+           Spec_Rules.add_global Spec_Rules.Equational ([head], [def_thm])
+           #> Code.add_eqn (Code.Equation, true) def_thm)
       end;
 
     fun add_corr (s, (vs, prf)) thy =