1.1 --- a/test/Tools/isac/IsacKnowledge/complex.sml	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/complex.sml	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4   (*---  (1.1 + 2.2 I) * (3.3 + 4.4 I) = - 6.05 + 12 I  ---*)
     1.5   val t = str2term "(Float ((11,-1),(0,0)) + Float ((22,-1),(0,0)) * I__) *\
     1.6  		 \(Float ((33,-1),(0,0)) + Float ((44,-1),(0,0)) * I__)";
     1.7 - val Some (t',_) = 
     1.8 + val SOME (t',_) = 
     1.9       rewrite_set_ thy false 
    1.10  		  (append_rls "simpl_complex" make_polynomial 
    1.11  			      [Thm ("square_I", num_str square_I)]) t;