| changeset 42361 | 23f352990944 |
| parent 41302 | 0485186839a7 |
| child 46497 | 89ccf66aa73d |
--- a/src/HOL/Tools/SMT/smt_utils.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_utils.ML Sat Apr 16 16:15:37 2011 +0200 @@ -162,7 +162,7 @@ (* certified terms *) -fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt) fun typ_of ct = #T (Thm.rep_cterm ct)