1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -232,7 +232,7 @@
     1.4                                               (Logic.count_prems r', [], r'));
     1.5  case p' of
     1.6      [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) 
     1.7 -      $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
     1.8 +      $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
     1.9    | _ => error "rewrite.sml assumption changed";
    1.10  "===== \<up>  make asms without Trueprop --- \<up> ";
    1.11  "----- step 4: get the (instantiated) RHS";
    1.12 @@ -377,12 +377,12 @@
    1.13  (*+*)case eval_is_multUnordered "testid" "" tm thy of
    1.14  (*+*)  SOME
    1.15  (*+*)    ("testidx \<up> 2 * x_",
    1.16 -(*+*)     Const ("HOL.Trueprop", _) $
    1.17 -(*+*)       (Const ("HOL.eq", _) $
    1.18 -(*+*)         (Const ("Poly.is_multUnordered", _) $
    1.19 -(*+*)           (Const ("Groups.times_class.times", _) $
    1.20 -(*+*)             (Const ("Transcendental.powr", _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
    1.21 -(*+*)         Const ("HOL.True", _))) => ()
    1.22 +(*+*)     Const (\<^const_name>\<open>Trueprop\<close>, _) $
    1.23 +(*+*)       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    1.24 +(*+*)         (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
    1.25 +(*+*)           (Const (\<^const_name>\<open>times\<close>, _) $
    1.26 +(*+*)             (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
    1.27 +(*+*)         Const (\<^const_name>\<open>True\<close>, _))) => ()
    1.28  (*+*)(*                   ^^^^^^             compare ---vvv *)
    1.29  (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
    1.30  
    1.31 @@ -392,7 +392,7 @@
    1.32  case eval_is_multUnordered "testid" "" tm thy of
    1.33      SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
    1.34                     (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    1.35 -                          (Const ("Poly.is_multUnordered", _) $ _) $ 
    1.36 +                          (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
    1.37                            Const (\<^const_name>\<open>True\<close>, _))) => ()
    1.38    | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
    1.39