test/Tools/isac/Minisubpbl/300-init-subpbl.sml
changeset 48790 98df8f6dc3f9
parent 48761 4162c4f6f897
child 59279 255c853ea2f0
     1.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Wed Dec 05 15:29:36 2012 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Wed Dec 05 15:56:38 2012 +0100
     1.3 @@ -36,14 +36,14 @@
     1.4  		      val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
     1.5  (*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;*)
     1.6  "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 
     1.7 -	                   (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
     1.8 +	                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
     1.9                     ((thy',srls), m,  (pt,(p,p_)), (sc,d), is);
    1.10  val thy = assoc_thy thy';
    1.11  l = [] orelse ((*init.in solve..Apply_Method...*)
    1.12  			         (last_elem o fst) p = 0 andalso snd p = Res) (*false*);
    1.13  (*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
    1.14      (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
    1.15 -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
    1.16 +"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
    1.17                       ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
    1.18  1 < length l (*true*);
    1.19  val up = drop_last l;