src/Tools/isac/Knowledge/Rational-WN.sml
branchisac-update-Isa09-2
changeset 38034 928cebc9c4aa
parent 38031 460c24a6a6ba
child 59184 831fa972f73b
     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));