1.1 --- a/test/Tools/isac/IsacKnowledge/atools.sml	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/atools.sml	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
     1.5  
     1.6  val t = str2term "x occurs_in x";
     1.7 -val Some (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
     1.8 +val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
     1.9  if (term2s t') = "x occurs_in x = True" then ()
    1.10  else raise error "atools.sml: x occurs_in x = True ???";
    1.11  
    1.12 @@ -37,14 +37,14 @@
    1.13  some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c");
    1.14  val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \
    1.15  		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
    1.16 -val Some (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
    1.17 +val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
    1.18  if term2str t' =
    1.19     "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
    1.20  else raise error "atools.sml: some_occur_in true";
    1.21  
    1.22  val t = str2term "some_of [c_3, c_4] occur_in \
    1.23  		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
    1.24 -val Some (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
    1.25 +val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
    1.26  if term2str t' =
    1.27     "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
    1.28  else raise error "atools.sml: some_occur_in false";
    1.29 @@ -54,7 +54,7 @@
    1.30  "----------- argument_of -----------------------------------------";
    1.31  "----------- argument_of -----------------------------------------";
    1.32  val t = str2term "argument_in (M_b x)";
    1.33 -val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
    1.34 +val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
    1.35  if term2s t' = "(argument_in M_b x) = x" then ()
    1.36  else raise error "atools.sml:(argument_in M_b x) = x  ???";
    1.37  
    1.38 @@ -89,7 +89,7 @@
    1.39  val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) = 
    1.40      str2term "filter_sameFunId (y' L) \
    1.41  	     \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
    1.42 -val Some (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";
    1.43 +val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";
    1.44  if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n                        y x = c + L * x]) =\n[y' x = c + L * x]" then ()
    1.45  else raise error "atools.slm diff.behav. in filter_sameFunId";
    1.46  
    1.47 @@ -112,7 +112,7 @@
    1.48  						   _ $ _) = t;
    1.49  
    1.50  
    1.51 -val Some (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";
    1.52 +val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";
    1.53  if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () 
    1.54  else raise error "atools.sml diff.behav. in eval_boollist2sum";
    1.55  
    1.56 @@ -121,7 +121,7 @@
    1.57  		      [Calc ("Atools.boollist2sum", eval_boollist2sum "")];
    1.58  val t = str2term 
    1.59         "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
    1.60 -case rewrite_set_ thy false srls_ t of Some _ => ()
    1.61 +case rewrite_set_ thy false srls_ t of SOME _ => ()
    1.62  | _ => raise error "atools.sml diff.rewrite boollist2sum";
    1.63  trace_rewrite:=false;
    1.64