--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Jul 24 00:24:00 2014 +0200
@@ -481,8 +481,8 @@
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: *)
- |> singleton (Proof_Context.export lthy' lthy)
|> 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))))