1.1 --- a/test/Tools/isac/ProgLang/listg.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/listg.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -16,7 +16,7 @@
1.4 atomty thm;
1.5 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;
1.6 if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then ()
1.7 -else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
1.8 +else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
1.9
1.10 val t = str2term "nth_ 1 [a,b,c,d,e]";
1.11 atomty t;
1.12 @@ -54,20 +54,20 @@
1.13 val thm = ("length_Nil_","");
1.14 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
1.15 if ct="1 + (1 + (1 + 0))"then()
1.16 -else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
1.17 +else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
1.18
1.19
1.20 val ct = "length_ [1,1,1]";
1.21 val rls = "list_rls";
1.22 val (ct,asm) = the (rewrite_set thy' false rls ct);
1.23 if ct="3"then()
1.24 -else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
1.25 +else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
1.26
1.27
1.28 val ct = "length_ [1,1,1]";
1.29 val t = (term_of o the o (parse ListG.thy)) ct;
1.30 val t = eval_listexpr_ ListG.thy list_rls t;
1.31 case t of Free ("3",_) => ()
1.32 -| _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
1.33 +| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
1.34
1.35