# HG changeset patch
# User wenzelm
# Date 1425682416 -3600
# Node ID 9f44d053b97256618a391e216303d012d6ef762c
# Parent  025f70f35daf7be12b2041f659a254947b79749d
clarified context;

diff -r 025f70f35daf -r 9f44d053b972 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Mar 06 23:52:57 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Mar 06 23:53:36 2015 +0100
@@ -235,7 +235,7 @@
         fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t)
         fun inst_of_matches tts =
           fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
-          |> snd |> Vartab.dest |> map (apply2 (Thm.global_cterm_of thy) o term_pair_of)
+          |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of ctxt2) o term_pair_of)
         val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems)
         val case_th =
           rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
diff -r 025f70f35daf -r 9f44d053b972 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 23:52:57 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 06 23:53:36 2015 +0100
@@ -869,7 +869,7 @@
 
 fun expand_tuples thy intro =
   let
-    val ctxt = Proof_Context.init_global thy
+    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
     val intro_t = Thm.prop_of intro'
     val concl = Logic.strip_imp_concl intro_t
@@ -877,7 +877,7 @@
     val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
     val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     fun rewrite_pat (ct1, ct2) =
-      (ct1, Thm.global_cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
+      (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
     val t_insts' = map rewrite_pat t_insts
     val intro'' = Thm.instantiate (T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
diff -r 025f70f35daf -r 9f44d053b972 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 06 23:52:57 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 06 23:53:36 2015 +0100
@@ -143,7 +143,7 @@
 
 fun introrulify thy ths = 
   let
-    val ctxt = Proof_Context.init_global thy
+    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val ((_, ths'), ctxt') = Variable.import true ths ctxt
     fun introrulify' th =
       let
@@ -158,14 +158,15 @@
           in
             (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
           end
-        val x = (Thm.global_cterm_of thy o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
-          Logic.dest_implies o Thm.prop_of) @{thm exI}
+        val x =
+          (Thm.cterm_of ctxt' o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
+            Logic.dest_implies o Thm.prop_of) @{thm exI}
         fun prove_introrule (index, (ps, introrule)) =
           let
             val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
               THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
               THEN (EVERY (map (fn y =>
-                rtac (Drule.cterm_instantiate [(x, Thm.global_cterm_of thy (Free y))] @{thm exI}) 1) ps))
+                rtac (Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}) 1) ps))
               THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
               THEN TRY (assume_tac ctxt' 1)
           in