1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 04 09:01:10 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed May 04 14:04:53 2011 +0200
     1.3 @@ -163,33 +163,30 @@
     1.4  
     1.5  (*iterated by nxt_me; there (the resulting) ptp dropped
     1.6    may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
     1.7 -(* val (ptp as (pt, pos as (p,p_))) = ptp;
     1.8 -   val (ptp as (pt, pos as (p,p_))) = (pt,ip);
     1.9 -   *)
    1.10  fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
    1.11 -    let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
    1.12 -			      probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.13 -    in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
    1.14 -       then case mI' of
    1.15 -	 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
    1.16 -       | _ => nxt_specif Model_Problem (pt, (p,Pbl))
    1.17 -       else let val cpI = if pI = e_pblID then pI' else pI;
    1.18 -		val cmI = if mI = e_metID then mI' else mI;
    1.19 -		val {ppc,prls,where_,...} = get_pbt cpI;
    1.20 -		val pre = check_preconds "thy 100820" prls where_ probl;
    1.21 -		val pb = foldl and_ (true, map fst pre);
    1.22 -		(*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)
    1.23 -		val (_,tac) =
    1.24 -		    nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    1.25 -			     (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
    1.26 +  let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
    1.27 +			  probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.28 +  in 
    1.29 +    if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
    1.30 +    then 
    1.31 +      case mI' of
    1.32 +	      ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
    1.33 +      | _ => nxt_specif Model_Problem (pt, (p,Pbl))
    1.34 +    else 
    1.35 +      let 
    1.36 +        val cpI = if pI = e_pblID then pI' else pI;
    1.37 +		    val cmI = if mI = e_metID then mI' else mI;
    1.38 +		    val {ppc, prls, where_, ...} = get_pbt cpI;
    1.39 +		    val pre = check_preconds "thy 100820" prls where_ probl;
    1.40 +		    val pb = foldl and_ (true, map fst pre);
    1.41 +		    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)
    1.42 +		    val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    1.43 +			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
    1.44  	    in case tac of
    1.45 -		   Apply_Method mI => 
    1.46 -(* val Apply_Method mI = tac;
    1.47 -   *)
    1.48 -		   nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
    1.49 -		 | _ => nxt_specif tac ptp end
    1.50 -    end;
    1.51 -
    1.52 +		       Apply_Method mI => 
    1.53 +		         nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
    1.54 +		     | _ => nxt_specif tac ptp end
    1.55 +   end;
    1.56  
    1.57  (*.specify a new method;
    1.58     WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)