diff -r 04419dff594c -r 70a1d102660d test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 14:39:52 2021 +0200
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 15:36:09 2021 +0200
@@ -231,7 +231,7 @@
      val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 
                                              (Logic.count_prems r', [], r'));
 case p' of
-    [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) 
+    [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) 
       $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
   | _ => error "rewrite.sml assumption changed";
 "===== \<up>  make asms without Trueprop --- \<up> ";
@@ -374,10 +374,10 @@
 eval_is_multUnordered "testid" "" tm thy;
 
 case eval_is_multUnordered "testid" "" tm thy of
-    SOME (_, Const ("HOL.Trueprop", _) $ 
-                   (Const ("HOL.eq", _) $
+    SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
+                   (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
                           (Const ("Poly.is_multUnordered", _) $ _) $ 
-                          Const ("HOL.True", _))) => ()
+                          Const (\<^const_name>\<open>True\<close>, _))) => ()
   | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
 
 tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
@@ -599,14 +599,14 @@
 
 (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
 (*+*)(*val rules =
-(*+*)   [Eval ("Rings.divide_class.divide", fn),
+(*+*)   [Eval (\<^const_name>\<open>divide\<close>, fn),
 (*+*)    Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
 (*+*)    :
-(*+*)    Eval ("HOL.eq", fn),
+(*+*)    Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
 (*+*)    Thm ("not_true", "(\<not> True) = False"),
 (*+*)    Thm ("not_false", "(\<not> False) = True"),
 (*+*)    :
-(*+*)    Eval ("Transcendental.powr", fn),
+(*+*)    Eval (\<^const_name>\<open>powr\<close>, fn),
 (*+*)    Eval ("RatEq.is_ratequation_in", fn)]:
 (*+*)   rule list*)
 (*+*)chk: term list -> term list -> term list * bool