test/Tools/isac/Knowledge/rational.sml
branchisac-update-Isa09-2
changeset 38034 928cebc9c4aa
parent 38031 460c24a6a6ba
child 38041 850aaf5b3744
     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);