test/Tools/isac/Minisubpbl/300-init-subpbl.sml
changeset 59755 fbaff8cf0179
parent 59753 7ad0b6cfd408
child 59767 c4acd312bd53
     1.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Fri Dec 20 09:57:45 2019 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Fri Dec 20 10:24:52 2019 +0100
     1.3 @@ -26,8 +26,8 @@
     1.4  "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
     1.5  
     1.6  "~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
     1.7 -val Appl m = applicable_in p pt m;
     1.8 -member op = specsteps mI; (*false*)
     1.9 +  val Appl m = applicable_in p pt tac;
    1.10 +  (*if*) Tactic.for_specify' m; (*false*)
    1.11  (*val Updated (cs' as (_,_,(_,p'))) =  loc_solve_ (mI,m) ptp;*)
    1.12  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
    1.13  (*val (msg, cs') =*)