# HG changeset patch
# User traytel
# Date 1415884453 -3600
# Node ID 1ae67039b14f66c8ca27942dbc4f9b3be6e75693
# Parent  87d4ce309e04b6ef1da6d519e8be33ff998c2b94
do not introduce consts too early unnecessarily

diff -r 87d4ce309e04 -r 1ae67039b14f src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Nov 12 19:30:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Nov 13 14:14:13 2014 +0100
@@ -531,11 +531,7 @@
               mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
                 def_thms rec_thm
               |> K |> Goal.prove_sorry lthy' [] [] user_eqn
-              |> singleton (Proof_Context.export lthy' lthy)
-              (* for code extraction from proof terms: *)
-              |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^
-                Long_Name.separator ^ simpsN ^
-                (if js = [0] then "" else "_" ^ string_of_int (j + 1))))
+              |> Thm.close_derivation)
             js;
       in
         (js, simp_thms)