clarified context;

--- a/src/HOL/Tools/TFL/rules.ML	Mon Jun 01 16:07:38 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon Jun 01 17:08:47 2015 +0200
@@ -33,7 +33,7 @@
   val IMP_TRANS: thm -> thm -> thm
   val PROVE_HYP: thm -> thm -> thm
 
-  val CHOOSE: cterm * thm -> thm -> thm
+  val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
   val EXISTS: cterm * cterm -> thm -> thm
   val EXISTL: cterm list -> thm -> thm
   val IT_EXISTS: (cterm*cterm) list -> thm -> thm
@@ -337,13 +337,12 @@
  *
  *---------------------------------------------------------------------------*)
 
-fun CHOOSE (fvar, exth) fact =
+fun CHOOSE ctxt (fvar, exth) fact =
   let
     val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
     val redex = Dcterm.capply lam fvar
-    val thy = Thm.theory_of_cterm redex
     val t$u = Thm.term_of redex
-    val residue = Thm.global_cterm_of thy (Term.betapply (t, u))
+    val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
   in
     GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg

--- a/src/HOL/Tools/TFL/tfl.ML	Mon Jun 01 16:07:38 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Jun 01 17:08:47 2015 +0200
@@ -666,7 +666,7 @@
             val recursive_thms = map mk news
             val build_exists = Library.foldr
                                 (fn((x,t), th) =>
-                                 Rules.CHOOSE (tych x, Rules.ASSUME (tych t)) th)
+                                 Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th)
             val thms' = ListPair.map build_exists (vexl, recursive_thms)
             val same_concls = Rules.EVEN_ORS thms'
         in Rules.DISJ_CASESL thm' same_concls
@@ -695,7 +695,7 @@
  in
  Rules.GEN (tych a)
        (Rules.RIGHT_ASSOC ctxt
-          (Rules.CHOOSE(tych v, ex_th0)
+          (Rules.CHOOSE ctxt (tych v, ex_th0)
                 (mk_case ty_info (vname::aname::names)
                  thy {path=[v], rows=rows})))
  end end;
@@ -810,10 +810,10 @@
  *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
  *
  *---------------------------------------------------------------------------*)
-fun LEFT_ABS_VSTRUCT tych thm =
+fun LEFT_ABS_VSTRUCT ctxt tych thm =
   let fun CHOOSER v (tm,thm) =
         let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
-        in (ex_tm, Rules.CHOOSE(tych v, Rules.ASSUME (tych ex_tm)) thm)
+        in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm)
         end
       val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
       val {lhs,rhs} = USyntax.dest_eq veq
@@ -854,7 +854,7 @@
     val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
     val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
                           (substs, proved_cases)
-    val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
+    val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
     val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
     val dc = Rules.MP Sinduct dant
     val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))