1.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 10:01:18 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 10:10:26 2010 +0200
1.3 @@ -282,7 +282,7 @@
1.4 val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
1.5
1.6 val (i,is) = (~1,[2]);
1.7 - val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
1.8 + val ttt = Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
1.9 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
1.10 Free ((str_of_int o abs) i, HOLogic.realT)) $
1.11 powerproduct2term(is, vs);