test/Tools/isac/Knowledge/inssort.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37991 028442673981
child 38063 d2bdc4095e73
     1.1 --- a/test/Tools/isac/Knowledge/inssort.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/inssort.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  val rls = "ins_sort";
     1.5  val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct);
     1.6  if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK"
     1.7 -else raise error "sort [1,4,3,2] didn't work";
     1.8 +else error "sort [1,4,3,2] didn't work";
     1.9  
    1.10  
    1.11  "---------------- sort [1,3,2] by rewrite stepwise ----------------";
    1.12 @@ -83,7 +83,7 @@
    1.13  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
    1.14  (*val ct = "[#1, #2, #3]"*)
    1.15  if ct="[1, 2, 3]" then "sort [1,3,2] OK"
    1.16 -else raise error "sort [1,3,2] didn't work";
    1.17 +else error "sort [1,3,2] didn't work";
    1.18  
    1.19  
    1.20  "---------------- sort [1,3,2] from script ----------------";