1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  FROM val oris = prep_ori...
     1.5  TO   val (oris, _) = prep_ori...
     1.6  *)
     1.7 -"----- insert ctxt in ptree";
     1.8 +"----- insert ctxt in ctree";
     1.9  (* datatype ppobj
    1.10  FROM loc   : istate option * istate option,
    1.11  TO   loc   : (istate * ctxt) option * (istate * ctxt) option,
    1.12 @@ -497,7 +497,7 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.14  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.15  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.16 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) = 
    1.17 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = 
    1.18                              (nxt, p, [], pt);
    1.19  val ("ok", (_, _, ptp))  = locatetac tac (pt,p)
    1.20  val (pt, p) = ptp;
    1.21 @@ -546,7 +546,7 @@
    1.22  "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
    1.23      cas = NONE; (*true*)
    1.24  	      val hdl = pblterm dI pI;
    1.25 -        val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.26 +        val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.27  				  (pors, (dI, pI, mI), hdl)
    1.28          val pt = update_ctxt pt [] pctxt;
    1.29  
    1.30 @@ -604,7 +604,7 @@
    1.31  	        (*                   ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
    1.32  	        (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
    1.33                                                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
    1.34 -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) =
    1.35 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
    1.36    (CompleteSubpbl, [], (pt',pos'));
    1.37  p = ([], Res) = false;
    1.38  member op = [Pbl,Met] p_ = false;
    1.39 @@ -617,7 +617,7 @@
    1.40  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.41  	        val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
    1.42  (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
    1.43 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), 
    1.44 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), 
    1.45    (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.46  l = [] = false;
    1.47  nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
    1.48 @@ -651,7 +651,7 @@
    1.49  existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
    1.50  apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
    1.51  apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
    1.52 -(append_atomic p ist_res f r f' s) : ptree -> ptree;
    1.53 +(append_atomic p ist_res f r f' s) : ctree -> ctree;
    1.54  ;
    1.55  (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
    1.56    getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR>  <<<<<=========================*)