1.1 --- a/src/Tools/isac/Interpret/appl.sml	Fri May 20 14:08:14 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri May 20 14:49:07 2011 +0200
     1.3 @@ -347,26 +347,21 @@
     1.4              if is_e_ctxt ctxt
     1.5              then assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres
     1.6              else ctxt
     1.7 -    (*TODO.WN110416 here do evalprecond according to fun check_preconds'
     1.8 -      and then decide on Notappl/Appl accordingly once more.
     1.9 -      Implement after all tests are running, since this changes
    1.10 -      overall system behavior*)
    1.11 -  in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
    1.12 +         (*TODO.WN110416 here do evalprecond according to fun check_preconds'
    1.13 +         and then decide on Notappl/Appl accordingly once more.
    1.14 +         Implement after all tests are running, since this changes
    1.15 +         overall system behavior*)
    1.16 +      in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
    1.17  
    1.18    | applicable_in (p,p_) pt (Check_Postcond pI) =
    1.19 -  if member op = [Pbl,Met] p_                  
    1.20 -    then Notappl ((tac2str (Check_Postcond pI)) ^
    1.21 -	   " not for pos "^(pos'2str (p,p_)))
    1.22 -  else Appl (Check_Postcond' 
    1.23 -		 (pI,(e_term,[(*asm in solve*)])))
    1.24 -  (* in solve -"-     ^^^^^^ gets returnvalue of scr*)
    1.25 +      if member op = [Pbl,Met] p_                  
    1.26 +      then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
    1.27 +      else Appl (Check_Postcond' (pI, (e_term, [(*in solve assigned the returnvalue of scr*)])))
    1.28  
    1.29    (*these are always applicable*)
    1.30    | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
    1.31    | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
    1.32  
    1.33 -(* val m as Rewrite_Inst (subs, thm') = m;
    1.34 -   *)
    1.35    | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) = 
    1.36    if member op = [Pbl,Met] p_ 
    1.37      then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))