1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Fri Mar 04 11:30:37 2011 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Fri Mar 04 11:43:45 2011 +0100
     1.3 @@ -180,7 +180,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 ("Not", _) $ (Const ("op =", _) $ Free ("y", _) $
     1.8 +    [Const ("Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
     1.9                                 Const ("Groups.zero_class.zero", _))] => ()
    1.10    | _ => error "rewrite.sml assumption changed";
    1.11  "=====^^^ make asms without Trueprop ---^^^";
    1.12 @@ -441,7 +441,7 @@
    1.13  val tm = str2term "(x^^^2 * x) is_multUnordered";
    1.14  case eval_is_multUnordered "testid" "" tm thy of
    1.15      SOME (_, Const ("Trueprop", _) $ 
    1.16 -                   (Const ("op =", _) $
    1.17 +                   (Const ("HOL.eq", _) $
    1.18                            (Const ("Poly.is'_multUnordered", _) $ _) $ 
    1.19                            Const ("True", _))) => ()
    1.20    | _ => error "rewrite.sml diff. eval_is_multUnordered 2";