--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Nov 13 12:35:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Nov 13 14:40:06 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)