--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Mar 04 19:53:18 2015 +0100
@@ -78,10 +78,10 @@
let
val thy = Proof_Context.theory_of ctxt;
val fs = Misc_Legacy.term_frees eq;
- val cvs = cterm_of thy (HOLogic.mk_list T fs);
- val clhs = cterm_of thy (reif_polex T fs lhs);
- val crhs = cterm_of thy (reif_polex T fs rhs);
- val ca = ctyp_of thy T;
+ val cvs = Thm.cterm_of thy (HOLogic.mk_list T fs);
+ val clhs = Thm.cterm_of thy (reif_polex T fs lhs);
+ val crhs = Thm.cterm_of thy (reif_polex T fs rhs);
+ val ca = Thm.ctyp_of thy 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";