--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Mar 06 23:14:41 2015 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Mar 06 23:33:25 2015 +0100
@@ -76,12 +76,11 @@
fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
let
- val thy = Proof_Context.theory_of ctxt;
val fs = Misc_Legacy.term_frees eq;
- val cvs = Thm.global_cterm_of thy (HOLogic.mk_list T fs);
- val clhs = Thm.global_cterm_of thy (reif_polex T fs lhs);
- val crhs = Thm.global_cterm_of thy (reif_polex T fs rhs);
- val ca = Thm.global_ctyp_of thy T;
+ val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs);
+ val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs);
+ val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs);
+ val ca = Thm.ctyp_of ctxt T;
in (ca, cvs, clhs, crhs) end
else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
| reif_eq _ _ = error "reif_eq: not an equation";