--- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Fri Mar 06 15:58:56 2015 +0100
@@ -468,7 +468,7 @@
fun conv ctxt t =
let
val ([t'], ctxt') = Variable.import_terms true [t] (Variable.declare_term t ctxt)
- val ct = Proof_Context.cterm_of ctxt' t'
+ val ct = Thm.cterm_of ctxt' t'
fun unfold_conv thms =
Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
(empty_simpset ctxt' addsimps thms)
@@ -498,7 +498,7 @@
val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong)))
in
- cterm_instantiate [(Proof_Context.cterm_of ctxt f, Proof_Context.cterm_of ctxt pred)] arg_cong
+ cterm_instantiate [(Thm.cterm_of ctxt f, Thm.cterm_of ctxt pred)] arg_cong
end;
fun simproc ctxt redex =