1.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -76,8 +76,8 @@
     1.4  "~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =
     1.5    ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
     1.6  
     1.7 -term2str e1 = "Try (Rewrite_Set ''norm_equation'' False)"  (*in isabisac*);
     1.8 -term2str e1 = "Try (Rewrite_Set norm_equation False)"      (*in isabisacREP*);
     1.9 +term2str e1 = "Try (Rewrite_Set ''norm_equation'')"  (*in isabisac*);
    1.10 +term2str e1 = "Try (Rewrite_Set norm_equation)"      (*in isabisacREP*);
    1.11  termopt2str a = "(SOME e_e)"  (*in isabisac + isabisacREP*);
    1.12  
    1.13  (*val Assoc (scrstate, steps) =    in isabisacREP*)
    1.14 @@ -96,7 +96,7 @@
    1.15  (*val NotAss =     in isabisac*)
    1.16  (*case*) associate pt ctxt (m, stac) (*of*);
    1.17  "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))), 
    1.18 -      (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_)) = (pt, d, m, stac);
    1.19 +      (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);
    1.20  
    1.21  if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
    1.22  
    1.23 @@ -132,10 +132,9 @@
    1.24  (*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v    ERROR go: no [L,L,R]*)
    1.25  (*isabisac17:                                        (go up sc)        ERROR go: no [L,L,R]*)
    1.26  (*isabisac15:*)
    1.27 -val ttt as Const ("Tactical.Try", _) $ (Const ("Prog_Tac.Rewrite'_Set", _) $ rls $
    1.28 -  Const ("HOL.False", _)) = (go up sc)
    1.29 +val ttt as Const ("Tactical.Try", _) $ (Const ("Prog_Tac.Rewrite'_Set", _) $ rls) = (go up sc)
    1.30  val (Const ("Tactical.Try"(*2*), _) $ _) = ttt;
    1.31 -if term2str ttt = "Try (Rewrite_Set ''norm_equation'' False)"
    1.32 +if term2str ttt = "Try (Rewrite_Set ''norm_equation'')"
    1.33  then () else error "250-Rewrite_Set: (go up sc) CHANGED";
    1.34  
    1.35  "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Tactical.Try"(*2*), _) $ _), a, v) =