# 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