1.1 --- a/test/Tools/isac/Interpret/script.sml	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -231,9 +231,9 @@
     1.4  member op = specsteps mI; (*false*)
     1.5  (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
     1.6  loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
     1.7 -(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
     1.8 +(*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
     1.9  (mI,m); (*string * tac*)
    1.10 -ptp (*ptree * pos'*);
    1.11 +ptp (*ctree * pos'*);
    1.12  "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
    1.13  (*val (msg, cs') = solve m (pt, pos);
    1.14  (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
    1.15 @@ -315,7 +315,7 @@
    1.16                                   (*WAS stac2tac_ TODO: no match for SubProblem*)
    1.17  val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.18  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.19 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)), 
    1.20 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
    1.21  	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.22  l; (*= [R, L, R, L, R, R]*)
    1.23  val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
    1.24 @@ -348,7 +348,7 @@
    1.25            | _ => error "integrate.sml -- me method [diff,integration] -- spec";
    1.26  "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
    1.27  
    1.28 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
    1.29 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
    1.30  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
    1.31  val (mI,m) = mk_tac'_ tac;
    1.32  val Appl m = applicable_in p pt m;
    1.33 @@ -366,7 +366,7 @@
    1.34  ini = NONE; (*true*)
    1.35              val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
    1.36  	            val d = e_rls (*FIXME: get simplifier from domID*);
    1.37 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 
    1.38 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
    1.39  	                     (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
    1.40                     ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
    1.41  val thy = assoc_thy thy';