1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -231,7 +231,7 @@
     1.4       val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 
     1.5                                               (Logic.count_prems r', [], r'));
     1.6  case p' of
     1.7 -    [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) 
     1.8 +    [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) 
     1.9        $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
    1.10    | _ => error "rewrite.sml assumption changed";
    1.11  "===== \<up>  make asms without Trueprop --- \<up> ";
    1.12 @@ -374,10 +374,10 @@
    1.13  eval_is_multUnordered "testid" "" tm thy;
    1.14  
    1.15  case eval_is_multUnordered "testid" "" tm thy of
    1.16 -    SOME (_, Const ("HOL.Trueprop", _) $ 
    1.17 -                   (Const ("HOL.eq", _) $
    1.18 +    SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
    1.19 +                   (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    1.20                            (Const ("Poly.is_multUnordered", _) $ _) $ 
    1.21 -                          Const ("HOL.True", _))) => ()
    1.22 +                          Const (\<^const_name>\<open>True\<close>, _))) => ()
    1.23    | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
    1.24  
    1.25  tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
    1.26 @@ -599,14 +599,14 @@
    1.27  
    1.28  (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
    1.29  (*+*)(*val rules =
    1.30 -(*+*)   [Eval ("Rings.divide_class.divide", fn),
    1.31 +(*+*)   [Eval (\<^const_name>\<open>divide\<close>, fn),
    1.32  (*+*)    Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
    1.33  (*+*)    :
    1.34 -(*+*)    Eval ("HOL.eq", fn),
    1.35 +(*+*)    Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
    1.36  (*+*)    Thm ("not_true", "(\<not> True) = False"),
    1.37  (*+*)    Thm ("not_false", "(\<not> False) = True"),
    1.38  (*+*)    :
    1.39 -(*+*)    Eval ("Transcendental.powr", fn),
    1.40 +(*+*)    Eval (\<^const_name>\<open>powr\<close>, fn),
    1.41  (*+*)    Eval ("RatEq.is_ratequation_in", fn)]:
    1.42  (*+*)   rule list*)
    1.43  (*+*)chk: term list -> term list -> term list * bool