1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Fri Mar 04 11:30:37 2011 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Fri Mar 04 11:43:45 2011 +0100
     1.3 @@ -397,7 +397,7 @@
     1.4  (*.for evaluation of conditions in rewrite rules.*)
     1.5  val Poly_erls = 
     1.6      append_rls "Poly_erls" Atools_erls
     1.7 -               [ Calc ("op =",eval_equal "#equal_"),
     1.8 +               [ Calc ("HOL.eq",eval_equal "#equal_"),
     1.9  		 Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
    1.10                   Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.11  		 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
    1.12 @@ -407,7 +407,7 @@
    1.13  
    1.14  val poly_crls = 
    1.15      append_rls "poly_crls" Atools_crls
    1.16 -               [ Calc ("op =",eval_equal "#equal_"),
    1.17 +               [ Calc ("HOL.eq",eval_equal "#equal_"),
    1.18  		 Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),
    1.19                   Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.20  		 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),