1.1 --- a/test/Tools/isac/Interpret/script.sml	Thu Jul 24 15:44:50 2014 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Thu Jul 24 17:22:21 2014 +0200
     1.3 @@ -176,8 +176,8 @@
     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", "Biegelinie.Belastung_Querkraft"))
     1.8 -then () else error "";
     1.9 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x"))
    1.10 +then () else error "--- WN0509 Substitute 2nd part --- changed";
    1.11  
    1.12  
    1.13  "----------- fun sel_appl_atomic_tacs ----------------------------";
    1.14 @@ -196,11 +196,8 @@
    1.15  val ((pt, p), _) = get_calc 1; show_pt pt;
    1.16  val appltacs = sel_appl_atomic_tacs pt p;
    1.17  if appltacs = 
    1.18 -(* WN130613
    1.19 -   [Rewrite ("radd_commute", "Test.radd_commute") (*"?m + ?n = ?n + ?m"*),
    1.20 -    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), Calculate "TIMES"] *)
    1.21 -   [Rewrite ("radd_commute", "Test.radd_commute"), 
    1.22 -    Rewrite ("add_assoc", "Groups.semigroup_add_class.add_assoc"), Calculate "TIMES"]
    1.23 +  [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), 
    1.24 +  Rewrite ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"), Calculate "TIMES"]
    1.25  then () else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
    1.26  
    1.27  trace_script := true;