1.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri Apr 08 15:16:08 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Apr 11 12:56:57 2011 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  
     1.6  fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
     1.7 -    (tac_2tac tac_, tac_, (p, get_istate pt p)):taci;
     1.8 +    (tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
     1.9  
    1.10  
    1.11  (*FIXME.WN050821 compare solve ... nxt_solv*)
    1.12 @@ -204,12 +204,12 @@
    1.13  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    1.14        val metID = get_obj g_metID pt pp;
    1.15        val {srls=srls,scr=sc,...} = get_met metID;
    1.16 -      val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_); 
    1.17 +      val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
    1.18       (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
    1.19        val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
    1.20        val thy' = get_obj g_domID pt pp;
    1.21        val thy = assoc_thy thy';
    1.22 -      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
    1.23 +      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
    1.24        (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
    1.25  
    1.26      in if pp = [] then
    1.27 @@ -226,7 +226,7 @@
    1.28          val thy = assoc_thy thy';
    1.29  	val metID = get_obj g_metID pt ppp;
    1.30          val sc = (#scr o get_met) metID;
    1.31 -        val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm); 
    1.32 +        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm); 
    1.33       (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
    1.34    	val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
    1.35    	val _=tracing("### solve Check_postc, is'= "^
    1.36 @@ -271,7 +271,7 @@
    1.37  	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
    1.38  	tac_2tac tac_, Sundef,*)
    1.39  	[(End_Detail, End_Detail' t , 
    1.40 -	  ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end
    1.41 +	  ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) end
    1.42  
    1.43    | solve (mI,m) (pt, po as (p,p_)) =
    1.44  (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    1.45 @@ -360,12 +360,12 @@
    1.46  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    1.47        val metID = get_obj g_metID pt pp;
    1.48        val {srls=srls,scr=sc,...} = get_met metID;
    1.49 -      val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_); 
    1.50 +      val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
    1.51       (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
    1.52        val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
    1.53        val thy' = get_obj g_domID pt pp;
    1.54        val thy = assoc_thy thy';
    1.55 -      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
    1.56 +      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
    1.57        (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
    1.58      in if pp = [] then 
    1.59  	   let val is = ScrState (E,l,a,scval,scsaf,b)
    1.60 @@ -383,7 +383,7 @@
    1.61          val thy = assoc_thy thy';
    1.62  	val metID = get_obj g_metID pt ppp;
    1.63  	val {scr,...} = get_met metID;
    1.64 -        val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm)
    1.65 +        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm)
    1.66          val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
    1.67  	val is = ScrState (E,l,a,scval,scsaf,b)
    1.68      (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";