1.1 --- a/src/Tools/isac/ProgLang/termC.sml	Tue Sep 28 10:01:18 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Tue Sep 28 10:10:26 2010 +0200
     1.3 @@ -565,7 +565,7 @@
     1.4    | num_of_term t = error ("num_of_term not for "^term2str t);
     1.5  
     1.6  fun mk_factroot op_(*=thy.sqrt*) T fact root = 
     1.7 -  Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
     1.8 +  Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $
     1.9    (Const (op_, T --> T) $ term_of_num T root);
    1.10  (*
    1.11  val T =  (type_of o term_of o the) (parse thy "#12::real");
    1.12 @@ -608,7 +608,7 @@
    1.13  (*used for calculating built in binary operations in Isabelle2002->Float.ML*)
    1.14  (*fun calc "Groups.plus_class.plus"  (n1, n2) = n1+n2
    1.15    | calc "Groups.minus_class.minus"  (n1, n2) = n1-n2
    1.16 -  | calc "op *"  (n1, n2) = n1*n2
    1.17 +  | calc "Groups.times_class.times"  (n1, n2) = n1*n2
    1.18    | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
    1.19    | calc "Atools.pow"(n1, n2) = power n1 n2
    1.20    | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
    1.21 @@ -1159,10 +1159,10 @@
    1.22    use length (vars term) = 1 instead*)
    1.23  fun is_atom (Const ("Float.Float",_) $ _) = true
    1.24    | is_atom (Const ("ComplexI.I'_'_",_)) = true
    1.25 -  | is_atom (Const ("op *",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
    1.26 +  | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
    1.27    | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
    1.28    | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ 
    1.29 -		   (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = 
    1.30 +		   (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_))) = 
    1.31      is_atom t1 andalso is_atom t2
    1.32    | is_atom (Const _) = true
    1.33    | is_atom (Free _) = true
    1.34 @@ -1182,7 +1182,7 @@
    1.35  > is_atom t;
    1.36  val it = true : bool
    1.37  > val t = str2term "1 + 2*I__";
    1.38 -> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("op *",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
    1.39 +> val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;
    1.40  *)
    1.41  
    1.42  (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's