1.1 --- a/test/Tools/isac/Scripts/rewrite.sml	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/test/Tools/isac/Scripts/rewrite.sml	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -158,19 +158,19 @@
     1.4  "----------- rewrite_terms_  -------------------------------------";
     1.5  val subte = [str2term"x = 0"];
     1.6  val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
     1.7 -val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
     1.8 +val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
     1.9  if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.10  else raise error "rewrite.sml rewrite_terms_ [x = 0]";
    1.11  
    1.12  val subte = [str2term"M_b 0 = 0"];
    1.13  val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
    1.14 -val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
    1.15 +val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
    1.16  if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.17  else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
    1.18  
    1.19  val subte = [str2term"x = 0", str2term"M_b 0 = 0"];
    1.20  val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
    1.21 -val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
    1.22 +val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
    1.23  if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.24  else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
    1.25  
    1.26 @@ -185,7 +185,7 @@
    1.27  	    (str2term"bdv_3",str2term"c_3"),
    1.28  	    (str2term"bdv_4",str2term"c_4")];
    1.29  (*------------ outcommented WN071210, after inclusion into ROOT.ML 
    1.30 -val Some (t,_) = 
    1.31 +val SOME (t,_) = 
    1.32      rewrite_inst_ thy e_rew_ord 
    1.33  		  (append_rls "erls_isolate_bdvs" e_rls 
    1.34  			      [(Calc ("EqSystem.occur'_exactly'_in",