test/Tools/isac/Knowledge/root.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37960 ec20007095f2
child 41943 f33f6959948b
     1.1 --- a/test/Tools/isac/Knowledge/root.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/root.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -5,11 +5,11 @@
     1.4  
     1.5  val t = str2term "sqrt 1";
     1.6  val SOME (t',_) = rewrite_set_ thy false Root_erls t;
     1.7 -if term2str t' = "1" then () else raise error "root.sml: diff.behav. sqrt 1";
     1.8 +if term2str t' = "1" then () else error "root.sml: diff.behav. sqrt 1";
     1.9  val t = str2term "sqrt -1";
    1.10  val NONE = rewrite_set_ thy false Root_erls t;
    1.11  
    1.12  val t = str2term "sqrt 0";
    1.13  val SOME (t',_) = rewrite_set_ thy false Root_erls t;
    1.14  term2str t';
    1.15 -if term2str t' = "0" then () else raise error "root.sml: diff.behav. sqrt 1";
    1.16 +if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1";