1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sat Apr 16 10:19:45 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Mon Apr 18 14:43:26 2011 +0200
     1.3 @@ -349,15 +349,15 @@
     1.4      val pres = map (mk_env probl |> subst_atomic) where_
     1.5      val ctxt = assoc_thy dI |> ProofContext.init_global 
     1.6            |> insert_assumptions pres
     1.7 -    (*TODO.WN110416 here evalprecond according to fun check_preconds'
     1.8 -      and then decide on Notappl/Appl once more.
     1.9 +    (*TODO.WN110416 here do evalprecond according to fun check_preconds'
    1.10 +      and then decide on Notappl/Appl accordingly once more.
    1.11        Implement after all tests are running, since this changes
    1.12        overall system behavior*)
    1.13    in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
    1.14  
    1.15    | applicable_in (p,p_) pt (Check_Postcond pI) =
    1.16    if member op = [Pbl,Met] p_                  
    1.17 -    then Notappl ((tac2str (Check_Postcond pI))^
    1.18 +    then Notappl ((tac2str (Check_Postcond pI)) ^
    1.19  	   " not for pos "^(pos'2str (p,p_)))
    1.20    else Appl (Check_Postcond' 
    1.21  		 (pI,(e_term,[(*asm in solve*)])))