--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 03 19:08:04 2015 +0100
@@ -273,7 +273,7 @@
HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero);
val thm =
Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
- mk_size_neq ctxt (map (certify lthy2) xs)
+ mk_size_neq ctxt (map (Proof_Context.cterm_of lthy2) xs)
(#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
|> single
|> Proof_Context.export names_lthy2 lthy2