1.1 --- a/test/Tools/isac/Knowledge/poly.sml	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -339,13 +339,13 @@
     1.4  val t = TermC.str2term "x \<up> 2 * x";
     1.5  val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
     1.6  if UnparseC.term t' = "x * x \<up> 2" then ()
     1.7 -else error "poly.sml Poly.is'_multUnordered doesn't work";
     1.8 +else error "poly.sml Poly.is_multUnordered doesn't work";
     1.9  
    1.10  (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
    1.11  ###  rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +
    1.12   (-48 * x \<up> 4 + 8))
    1.13  ######  rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
    1.14 -#######  try calc: Poly.is'_multUnordered'
    1.15 +#######  try calc: Poly.is_multUnordered'
    1.16  =======  calc. to: False  !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
    1.17  *)
    1.18  val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +  (-48 * x \<up> 4 + 8))";
    1.19 @@ -363,7 +363,7 @@
    1.20  case eval_is_multUnordered "testid" "" tm thy of
    1.21      SOME (_, Const ("HOL.Trueprop", _) $ 
    1.22                     (Const ("HOL.eq", _) $
    1.23 -                          (Const ("Poly.is'_multUnordered", _) $ _) $ 
    1.24 +                          (Const ("Poly.is_multUnordered", _) $ _) $ 
    1.25                            Const ("HOL.True", _))) => ()
    1.26    | _ => error "poly.sml diff. eval_is_multUnordered";
    1.27