test/Tools/isac/ProgLang/calculate.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38022 e6d356fc4d38
child 38032 121765ba0a34
     1.1 --- a/test/Tools/isac/ProgLang/calculate.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  val SOME (thmID, thm) = get_calculation_ thy cal t;
     1.5  (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")
     1.6  handle TERM _ => 
     1.7 -       raise error "calculate.sml: get_calculation_ must return Trueprop";
     1.8 +       error "calculate.sml: get_calculation_ must return Trueprop";
     1.9  
    1.10  
    1.11  
    1.12 @@ -66,7 +66,7 @@
    1.13  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.14  Sign.string_of_term (sign_of thy) t;
    1.15  (*val it = "#16" : string*)
    1.16 -if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
    1.17 +if it <> "16" then error "calculate.sml: new behaviour in calculate_"
    1.18  else ();
    1.19  
    1.20  " ================= calculate.sml: aus script ======================== ";
    1.21 @@ -140,7 +140,7 @@
    1.22  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.23  (*nxt = ("End_Proof'",End_Proof')*)
    1.24  if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
    1.25 -else raise error "calculate.sml: script test_calculate changed behaviour";
    1.26 +else error "calculate.sml: script test_calculate changed behaviour";
    1.27  
    1.28  
    1.29  
    1.30 @@ -421,7 +421,7 @@
    1.31   val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.32   Sign.string_of_term (sign_of thy) t;
    1.33  "16";
    1.34 - if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
    1.35 + if it <> "16" then error "calculate.sml: new behaviour in calculate_"
    1.36   else ();
    1.37  
    1.38  (*13.9.02 *** calc: operator = pow not defined*)
    1.39 @@ -458,7 +458,7 @@
    1.40  val Some (str, simpl) = get_pair thy op_ ef arg;
    1.41  if str = 
    1.42  "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
    1.43 -then () else raise error "calculate.sml get_pair with 3 args:occur_exactly_in";
    1.44 +then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";
    1.45  
    1.46  
    1.47