1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -29,26 +29,26 @@
     1.4  fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)
     1.5  fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)
     1.6    let val minus_1 = t |> type_of |> mk_minus_1
     1.7 -  in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
     1.8 +  in HOLogic.mk_binop \<^const_name>\<open>times\<close> (minus_1, t) end;
     1.9  \<close>
    1.10  
    1.11  text \<open>from solutions (e.g. [z = 1, z = -2]) make linear factors (e.g. (z - 1)*(z - -2))\<close>
    1.12  ML \<open>
    1.13  fun fac_from_sol s =
    1.14    let val (lhs, rhs) = HOLogic.dest_eq s
    1.15 -  in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
    1.16 +  in HOLogic.mk_binop \<^const_name>\<open>minus\<close> (lhs, rhs) end;
    1.17  
    1.18  fun mk_prod prod [] =
    1.19        if prod = TermC.empty then raise ERROR "mk_prod called with []" else prod
    1.20    | mk_prod prod (t :: []) =
    1.21 -      if prod = TermC.empty then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
    1.22 +      if prod = TermC.empty then t else HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t)
    1.23    | mk_prod prod (t1 :: t2 :: ts) =
    1.24          if prod = TermC.empty 
    1.25          then 
    1.26 -           let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
    1.27 +           let val p = HOLogic.mk_binop \<^const_name>\<open>times\<close> (t1, t2)
    1.28             in mk_prod p ts end 
    1.29          else 
    1.30 -           let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
    1.31 +           let val p = HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t1)
    1.32             in mk_prod p (t2 :: ts) end 
    1.33  
    1.34  fun factors_from_solution sol =