test/Tools/isac/Interpret/script.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37981 b2877b9d455a
child 38058 ad0485155c0e
     1.1 --- a/test/Tools/isac/Interpret/script.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4  atomty sc';
     1.5  val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
     1.6  (*---------------------------------------------------------------------
     1.7 -if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";
     1.8 +if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
     1.9  ---------------------------------------------------------------------*)
    1.10  
    1.11  val fmz = ["Traegerlaenge L",
    1.12 @@ -97,7 +97,7 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.14  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.15  case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
    1.16 -	  | _ => raise error "script.sml, doesnt find Substitute #2";
    1.17 +	  | _ => error "script.sml, doesnt find Substitute #2";
    1.18  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    1.19  (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
    1.20  (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
    1.21 @@ -109,7 +109,7 @@
    1.22  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    1.23  (*---------------------------------------------------------------------*)
    1.24  case nxt of (_, End_Proof') => () 
    1.25 -	  | _ => raise error "script.sml, doesnt find Substitute #3";
    1.26 +	  | _ => error "script.sml, doesnt find Substitute #3";
    1.27  (*---------------------------------------------------------------------*)
    1.28  (*the reason, that next_tac didnt find the 2nd Substitute, was that
    1.29    the Take inbetween was missing, and thus the 2nd Substitute was applied
    1.30 @@ -151,7 +151,7 @@
    1.31  
    1.32  val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
    1.33  (*---------------------------------------------------------------------
    1.34 -if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";
    1.35 +if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
    1.36  ---------------------------------------------------------------------*)
    1.37  val fmz = ["Traegerlaenge L",
    1.38  	   "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
    1.39 @@ -172,7 +172,7 @@
    1.40  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.41  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.42  case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
    1.43 -	  | _ => raise error "script.sml, doesnt find Substitute #2";
    1.44 +	  | _ => error "script.sml, doesnt find Substitute #2";
    1.45  trace_rewrite:=true;
    1.46  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
    1.47  trace_rewrite:=false;
    1.48 @@ -195,7 +195,7 @@
    1.49  val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";
    1.50  val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;
    1.51  if term2str e1__ = "M_b 0 = 0" then () else 
    1.52 -raise error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
    1.53 +error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";
    1.54  
    1.55  (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
    1.56  val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
    1.57 @@ -235,7 +235,7 @@
    1.58     [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
    1.59      Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
    1.60      Calculate "times"] then ()
    1.61 -else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";
    1.62 +else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
    1.63  
    1.64  trace_script := true;
    1.65  trace_script := false;