test/Tools/isac/Minisubpbl/150-add-given.sml
changeset 59426 c7b52bf9c8ae
parent 59279 255c853ea2f0
child 59749 cc3b1807f72e
     1.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue Apr 03 15:48:39 2018 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue Apr 03 16:53:18 2018 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  
     1.5  "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);
     1.6      val (pt, p) = 
     1.7 +      (*ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
     1.8  	    case locatetac tac (pt,p) of
     1.9  		    ("ok", (_, _, ptp)) => ptp;
    1.10  (*  val (_, ts) =