test/Tools/isac/Minisubpbl/300-init-subpbl.sml
changeset 59279 255c853ea2f0
parent 48790 98df8f6dc3f9
child 59361 76b3141b73ab
     1.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  	      val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
     1.5  		      val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
     1.6  (*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;*)
     1.7 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 
     1.8 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
     1.9  	                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
    1.10                     ((thy',srls), m,  (pt,(p,p_)), (sc,d), is);
    1.11  val thy = assoc_thy thy';