diff -r 95d956108461 -r 460c24a6a6ba test/Tools/isac/ProgLang/listg.sml
--- a/test/Tools/isac/ProgLang/listg.sml	Tue Sep 28 08:58:06 2010 +0200
+++ b/test/Tools/isac/ProgLang/listg.sml	Tue Sep 28 09:06:56 2010 +0200
@@ -16,7 +16,7 @@
 atomty thm;
 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm 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]";
+else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
 
 val t = str2term "nth_ 1 [a,b,c,d,e]";
 atomty t;
@@ -54,20 +54,20 @@
 val thm = ("length_Nil_","");
 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
 if ct="1 + (1 + (1 + 0))"then()
-else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
+else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
 
 
 val ct = "length_ [1,1,1]";
 val rls = "list_rls";
 val (ct,asm) = the (rewrite_set thy' false rls ct);
 if ct="3"then()
-else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
+else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
 
 
 val ct = "length_ [1,1,1]";
 val t = (term_of o the o (parse ListG.thy)) ct;
 val t = eval_listexpr_ ListG.thy list_rls t;
 case t of Free ("3",_) => () 
-| _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
+| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);