# HG changeset patch
# User wenzelm
# Date 1425682504 -3600
# Node ID a6d29266f01c67b4a170647cdfeb56adde5b3e70
# Parent  f596ed64701857ec161c00edb99602fd5ca0b640
clarified context;

diff -r f596ed647018 -r a6d29266f01c src/HOL/Tools/TFL/dcterm.ML
--- 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
diff -r f596ed647018 -r a6d29266f01c src/HOL/Tools/TFL/post.ML
--- 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 *)
diff -r f596ed647018 -r a6d29266f01c src/HOL/Tools/TFL/thry.ML
--- 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;