src/HOL/Library/comm_ring.ML

           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;
         in (ca, cvs, clhs, crhs) end
-      else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
+      else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
   | reif_eq _ _ = raise CRing "reif_eq: not an equation";
 
 (* The cring tactic *)
 (* Attention: You have to make sure that no t^0 is in the goal!! *)
 (* Use simply rewriting t^0 = 1 *)