1.1 --- a/test/Tools/isac/OLDTESTS/script.sml	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/script.sml	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -89,19 +89,19 @@
     1.4    ("Substitute", tac2tac_ pt p
     1.5     (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")]));
     1.6  "------- same_tacpbl + eval_to -------";
     1.7 -val Some(l1,t1) = same_tacpbl sc ll (mI1,m1);
     1.8 +val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
     1.9  loc_2str l1;
    1.10  (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
    1.11  Sign.string_of_term (sign_of DiffApp.thy) t1;
    1.12  (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
    1.13  
    1.14 -val Some(l2,t2) = same_tacpbl sc l1 (mI2,m2);
    1.15 +val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
    1.16  loc_2str l2;
    1.17  (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
    1.18  Sign.string_of_term (sign_of DiffApp.thy) t2;
    1.19  (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
    1.20  
    1.21 -val Some(l3,t3) = same_tacpbl sc l2 (mI3,m3);
    1.22 +val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
    1.23  loc_2str l3;
    1.24  (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
    1.25  Sign.string_of_term (sign_of DiffApp.thy) t3;