1.1 --- a/test/Tools/isac/Interpret/script.sml Thu Mar 08 14:33:34 2012 +0100
1.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Mar 10 09:41:09 2012 +0100
1.3 @@ -135,10 +135,9 @@
1.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.5 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.6 | _ => error "script.sml, doesnt find Substitute #2";
1.7 -
1.8 -(*========== inhibit exn AK110721 ================================================
1.9 (* ERROR: caused by f2str f *)
1.10 trace_rewrite:=true;
1.11 +
1.12 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
1.13 trace_rewrite:=false;
1.14 (*Exception TYPE raised:
1.15 @@ -155,22 +154,12 @@
1.16 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
1.17 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
1.18 thus corrected eval_argument_in OK*)
1.19 -========== inhibit exn AK110721 ================================================*)
1.20 -
1.21 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.22 -val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
1.23 +val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]";
1.24 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
1.25 -
1.26 -(*========== inhibit exn 110721 ================================================
1.27 -(*AK110722
1.28 - TRIAL: Should be the same
1.29 - term2str e1__e1 = "M_b 0 = 0";
1.30 - term2str e1__e1;*)
1.31 -
1.32 if term2str e1__e1 = "M_b 0 = 0"
1.33 then ()
1.34 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
1.35 -========== inhibit exn 110721 ================================================*)
1.36
1.37 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
1.38 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
1.39 @@ -180,16 +169,13 @@
1.40 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
1.41
1.42 val l__l = str2term "lhs (M_b 0 = 0)";
1.43 -(*AK110722 eval_listexpr_ is prob. without _ ????*)
1.44 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
1.45 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
1.46 -(*========== inhibit exn 110721 ================================================
1.47 -trace_rewrite:=true;
1.48 +
1.49 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
1.50 -trace_rewrite:=false;
1.51 -========== inhibit exn 110721 ================================================*)
1.52 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "Biegelinie.Belastung_Querkraft"))
1.53 +then () else error "";
1.54
1.55 -show_mets();
1.56
1.57 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.58 "----------- fun sel_appl_atomic_tacs ----------------------------";