1.1 --- a/src/Tools/isac/ProgLang/term.sml	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/term.sml	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -609,10 +609,10 @@
     1.4  *)
     1.5  
     1.6  (*used for calculating built in binary operations in Isabelle2002->Float.ML*)
     1.7 -(*fun calc "op +"  (n1, n2) = n1+n2
     1.8 -  | calc "op -"  (n1, n2) = n1-n2
     1.9 +(*fun calc "Groups.plus_class.plus"  (n1, n2) = n1+n2
    1.10 +  | calc "Groups.minus_class.minus"  (n1, n2) = n1-n2
    1.11    | calc "op *"  (n1, n2) = n1*n2
    1.12 -  | calc "HOL.divide"(n1, n2) = n1 div n2
    1.13 +  | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
    1.14    | calc "Atools.pow"(n1, n2) = power n1 n2
    1.15    | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
    1.16  fun calc_equ "op <"  (n1, n2) = n1 < n2
    1.17 @@ -1163,8 +1163,8 @@
    1.18  fun is_atom (Const ("Float.Float",_) $ _) = true
    1.19    | is_atom (Const ("ComplexI.I'_'_",_)) = true
    1.20    | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
    1.21 -  | is_atom (Const ("op +",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
    1.22 -  | is_atom (Const ("op +",_) $ t1 $ 
    1.23 +  | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
    1.24 +  | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ 
    1.25  		   (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = 
    1.26      is_atom t1 andalso is_atom t2
    1.27    | is_atom (Const _) = true
    1.28 @@ -1185,7 +1185,7 @@
    1.29  > is_atom t;
    1.30  val it = true : bool
    1.31  > val t = str2term "1 + 2*I__";
    1.32 -> val Const ("op +",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
    1.33 +> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
    1.34  *)
    1.35  
    1.36  (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's
    1.37 @@ -1214,6 +1214,6 @@
    1.38      let val T1 = type_of t1
    1.39  	val T2 = type_of t2
    1.40      in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2])
    1.41 -       else (Const ("op +", [T1, T2] ---> T1) $ t1 $ t2)
    1.42 +       else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
    1.43      end;
    1.44