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;