1.1 --- a/test/Tools/isac/Interpret/script.sml	Sun Oct 16 13:58:46 2016 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Tue Oct 18 12:05:03 2016 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
     1.5  
     1.6  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
     1.7 -if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x"))
     1.8 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", str2term "- qq ?x = Q' ?x"))
     1.9  then () else error "--- WN0509 Substitute 2nd part --- changed";
    1.10  
    1.11  
    1.12 @@ -195,10 +195,13 @@
    1.13  autoCalculate 1 (Step 1);
    1.14  val ((pt, p), _) = get_calc 1; show_pt pt;
    1.15  val appltacs = sel_appl_atomic_tacs pt p;
    1.16 -if appltacs = 
    1.17 -  [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), 
    1.18 -  Rewrite ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"), Calculate "TIMES"]
    1.19 -then () else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
    1.20 +case appltacs of 
    1.21 +  [Rewrite ("radd_commute", radd_commute), 
    1.22 +  Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
    1.23 +  => if term2str radd_commute = "?m + ?n = ?n + ?m" andalso 
    1.24 +        term2str add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
    1.25 +        else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
    1.26 +| _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
    1.27  
    1.28  trace_script := true;
    1.29  trace_script := false;