1.1 --- a/test/Tools/isac/IsacKnowledge/algein.sml	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/algein.sml	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -134,7 +134,7 @@
     1.4  
     1.5  val thm = assoc_thm' thy ("sym_real_mult_0_right","");
     1.6  val t = str2term "0 = 0";
     1.7 -val Some (t',_) = rewrite_ thy rew_ord erls false thm t;
     1.8 +val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
     1.9  term2str t';
    1.10  (********"0 = ?z1 * 0"*)
    1.11  
    1.12 @@ -150,7 +150,7 @@
    1.13  
    1.14  val thm = assoc_thm' thy ("sym","");
    1.15  (*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
    1.16 -val Some (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    1.17 +val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    1.18  *)
    1.19  
    1.20  (* use"../smltest/IsacKnowledge/algein.sml";