src/HOL/Library/comm_ring.ML

   | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
       polex_pow T $ reif_polex T vs a $ n
   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
 
 (* reification of the equation *)
-val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
+val cr_sort = @{sort "comm_ring_1"};
 
 fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
       if Sign.of_sort thy (T, cr_sort) then
         let
           val fs = OldTerm.term_frees eq;