src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     fn prem => fn additional_arguments =>
     let
       val [polarity, depth] = additional_arguments
       val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
       val depth' =
-        Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
-          $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
+        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
     in [polarity', depth'] end
   }
 
 val random_comp_modifiers = Comp_Mod.Comp_Modifiers
   {