1.1 --- a/test/Tools/isac/ProgLang/termC.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/termC.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -21,17 +21,17 @@
     1.4  "----------- inst_bdv -----------------------------------";
     1.5  if (term2str o prop_of o num_str) @{thm d1_isolate_add2} = 
     1.6      "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then ()
     1.7 -else raise error "termC.sml d1_isolate_add2";
     1.8 +else error "termC.sml d1_isolate_add2";
     1.9  val subst = [(str2term "bdv", str2term "x")];
    1.10  val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
    1.11  val t' = inst_bdv subst t;
    1.12  if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
    1.13 -else raise error "termC.sml inst_bdv 1";
    1.14 +else error "termC.sml inst_bdv 1";
    1.15  
    1.16  if string_of_thm (num_str @{thm separate_bdvs_add}) = 
    1.17     "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
    1.18     \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
    1.19 -else raise error "termC.sml separate_bdvs_add";
    1.20 +else error "termC.sml separate_bdvs_add";
    1.21  val subst = [(str2term"bdv_1",str2term"c"),
    1.22  	    (str2term"bdv_2",str2term"c_2"),
    1.23  	    (str2term"bdv_3",str2term"c_3"),
    1.24 @@ -40,7 +40,7 @@
    1.25  val t' = inst_bdv subst t;
    1.26  if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
    1.27  		 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
    1.28 -else raise error "termC.sml inst_bdv 2";
    1.29 +else error "termC.sml inst_bdv 2";
    1.30  
    1.31  
    1.32  "----------- subst_atomic_all ---------------------------";
    1.33 @@ -52,13 +52,13 @@
    1.34  val (all_Free_subst, t') = subst_atomic_all env t;
    1.35  if all_Free_subst andalso 
    1.36     term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
    1.37 -else raise error "termC.sml subst_atomic_all should be 'true'";
    1.38 +else error "termC.sml subst_atomic_all should be 'true'";
    1.39  
    1.40  
    1.41  val (all_Free_subst, t') = subst_atomic_all (tl env) t;
    1.42  if not all_Free_subst andalso 
    1.43     term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
    1.44 -else raise error "termC.sml subst_atomic_all should be 'false'";
    1.45 +else error "termC.sml subst_atomic_all should be 'false'";
    1.46  ===== inhibit exn ============================================================*)
    1.47  
    1.48