--- a/src/HOL/Tools/TFL/dcterm.ML Fri Mar 06 23:54:36 2015 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML Fri Mar 06 23:55:04 2015 +0100
@@ -67,7 +67,7 @@
* Some simple constructor functions.
*---------------------------------------------------------------------------*)
-val mk_hol_const = Thm.global_cterm_of @{theory HOL} o Const;
+val mk_hol_const = Thm.cterm_of @{theory_context HOL} o Const;
fun mk_exists (r as (Bvar, Body)) =
let val ty = Thm.typ_of_cterm Bvar
--- a/src/HOL/Tools/TFL/post.ML Fri Mar 06 23:54:36 2015 +0100
+++ b/src/HOL/Tools/TFL/post.ML Fri Mar 06 23:55:04 2015 +0100
@@ -72,8 +72,7 @@
fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
fun join_assums ctxt th =
- let val thy = Thm.theory_of_thm th
- val tych = Thm.global_cterm_of thy
+ let val tych = Thm.cterm_of ctxt
val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *)
--- a/src/HOL/Tools/TFL/thry.ML Fri Mar 06 23:54:36 2015 +0100
+++ b/src/HOL/Tools/TFL/thry.ML Fri Mar 06 23:55:04 2015 +0100
@@ -47,8 +47,8 @@
* Typing
*---------------------------------------------------------------------------*)
-fun typecheck thry t =
- Thm.global_cterm_of thry t
+fun typecheck thy t =
+ Thm.global_cterm_of thy t
handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
| TERM (msg, _) => raise THRY_ERR "typecheck" msg;