--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 03 19:08:04 2015 +0100
@@ -97,7 +97,7 @@
val fs = Term.add_vars (prop_of thm) []
|> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
fun mk_cfp (f as (_, T)) =
- (certify ctxt (Var f), certify ctxt (mk_proj T (num_binder_types T) k));
+ (Proof_Context.cterm_of ctxt (Var f), Proof_Context.cterm_of ctxt (mk_proj T (num_binder_types T) k));
val cfps = map mk_cfp fs;
in
Drule.cterm_instantiate cfps thm