--- a/src/HOL/Tools/Function/function_core.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Tue Mar 03 19:08:04 2015 +0100
@@ -183,7 +183,7 @@
val Globals {h, ...} = globals
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Proof_Context.cterm_of ctxt
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
val lGI = GIntro_thm
@@ -453,7 +453,7 @@
[] (* no special monos *)
||> Local_Theory.restore_naming lthy
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Proof_Context.cterm_of lthy
fun requantify orig_intro thm =
let
val (qs, t) = dest_all_all orig_intro
@@ -871,7 +871,7 @@
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Proof_Context.cterm_of lthy
val xclauses = PROFILE "xclauses"
(@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees