diff -r d957275620d4 -r e6fc98fbcb85 test/Tools/isac/Scripts/listg.sml
--- a/test/Tools/isac/Scripts/listg.sml	Wed Aug 18 13:53:15 2010 +0200
+++ b/test/Tools/isac/Scripts/listg.sml	Wed Aug 18 13:55:23 2010 +0200
@@ -14,7 +14,7 @@
 atomty t;
 val thm = (#prop o rep_thm o num_str) nth_Cons_;
 atomty thm;
-val Some (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t;
+val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t;
 if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
 else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
 
@@ -22,20 +22,20 @@
 atomty t;
 val thm = (#prop o rep_thm o num_str) nth_Nil_;
 atomty thm;
-val Some (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t;
+val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t;
 term2str t';
 "a";
 
 val t = str2term "nth_ 3 [a,b,c,d,e]";
 atomty t;
 trace_rewrite:=true;
-val Some (t',_) = rewrite_set_ thy false list_rls t;
+val SOME (t',_) = rewrite_set_ thy false list_rls t;
 trace_rewrite:=false;
 term2str t';
 "c";
 
 (*-------------------------------------------------------------------*)
-val Some (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
+val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
 val ttt = (#prop o rep_thm) thm;
 atomty ttt;
 (*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)