test/Tools/isac/ProgLang/listg.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37970 6df5d02e46ba
child 38058 ad0485155c0e
     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