changeset 59580 | cbc38731d42f |
parent 59498 | 50b60f501b05 |
child 59617 | b60e65ad13df |
--- a/src/HOL/Tools/code_evaluation.ML Tue Mar 03 17:20:51 2015 +0100 +++ b/src/HOL/Tools/code_evaluation.ML Tue Mar 03 19:08:04 2015 +0100 @@ -204,7 +204,7 @@ fun certify_eval ctxt value conv ct = let - val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); + val cert = Proof_Context.cterm_of ctxt; val t = Thm.term_of ct; val T = fastype_of t; val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));