1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 10:01:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Tue Sep 28 10:10:26 2010 +0200
1.3 @@ -57,7 +57,7 @@
1.4 fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
1.5 if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly
1.6 else error ("term2poly.1 "^term2str t1)
1.7 - | mono (t as Const ("op *",_) $ t1 $
1.8 + | mono (t as Const ("Groups.times_class.times",_) $ t1 $
1.9 (Const ("RatArith.pow",_) $ t2 $ t3)) v g =
1.10 if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1]
1.11 else error ("term2poly.2 "^term2str t)
1.12 @@ -71,7 +71,7 @@
1.13 fun term2poly (t as Free (s, _)) v =
1.14 if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]
1.15 handle _ => NONE)
1.16 - | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
1.17 + | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
1.18 if t = v then SOME [0, (the o int_of_str) s1] else NONE
1.19 | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v =
1.20 SOME ([(the o int_of_str) s1] @ (poly t v 1))
1.21 @@ -125,11 +125,11 @@
1.22 case g of
1.23 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)
1.24 | 1 => if c = 1 then Free (v, vT)
1.25 - else Const ("op *", [cT, vT]--->pT) $
1.26 + else Const ("Groups.times_class.times", [cT, vT]--->pT) $
1.27 Free (str_of_int c, cT) $ Free (v, vT)
1.28 | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $
1.29 Free (v, vT) $ Free (str_of_int g, eT))
1.30 - else Const ("op *", [cT, vT]--->pT) $
1.31 + else Const ("Groups.times_class.times", [cT, vT]--->pT) $
1.32 Free (str_of_int c, cT) $
1.33 (Const ("RatArith.pow", [vT, eT]--->pT) $
1.34 Free (v, vT) $ Free (str_of_int g, eT));