# HG changeset patch
# User haftmann
# Date 1497956863 -7200
# Node ID 4efbcc308ca017c9703df8438000dff4c22190a8
# Parent  8f1cbb77a70a1b14d4b1f306abbaf8c0a89b0a16
tuned

diff -r 8f1cbb77a70a -r 4efbcc308ca0 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Jun 20 17:31:29 2017 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jun 20 13:07:43 2017 +0200
@@ -789,35 +789,45 @@
       fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
         thm_vss [];
 
-    fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
-      (case Sign.const_type thy (extr_name s vs) of
-         NONE =>
-           let
-             val corr_prop = Reconstruct.prop_of prf;
-             val ft = Type.legacy_freeze t;
-             val fu = Type.legacy_freeze u;
-             val (def_thms, thy') = if t = nullt then ([], thy) else
-               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)), [])]
-           in
-             thy'
-             |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
-                  Thm.varifyT_global (funpow (length (vars_of corr_prop))
-                    (Thm.forall_elim_var 0) (Thm.forall_intr_frees
-                      (Proof_Checker.thm_of_proof thy'
-                       (fst (Proofterm.freeze_thaw_prf prf))))))
-             |> snd
-             |> fold (Code.add_eqn (Code.Equation, true)) def_thms
-           end
-       | SOME _ => thy);
+    fun add_def (s, (vs, ((t, u)))) thy =
+      let
+        val ft = Type.legacy_freeze t;
+        val fu = Type.legacy_freeze u;
+      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)
+      end;
+
+    fun add_corr (s, (vs, prf)) thy =
+      let
+        val corr_prop = Reconstruct.prop_of prf;
+      in
+        thy
+        |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
+            Thm.varifyT_global (funpow (length (vars_of corr_prop))
+              (Thm.forall_elim_var 0) (Thm.forall_intr_frees
+                (Proof_Checker.thm_of_proof thy
+                  (fst (Proofterm.freeze_thaw_prf prf))))))
+        |> snd
+      end;
+
+    fun add_def_and_corr (s, (vs, ((t, u), (prf, _)))) thy =
+      if is_none (Sign.const_type thy (extr_name s vs))
+      then
+        thy
+        |> not (t = nullt) ? add_def (s, (vs, ((t, u))))
+        |> add_corr (s, (vs, prf))
+      else
+        thy;
 
   in
     thy
     |> Sign.root_path
-    |> fold_rev add_def defs
+    |> fold_rev add_def_and_corr defs
     |> Sign.restore_naming thy
   end;