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