1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sun May 15 10:25:42 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sun May 15 11:32:41 2011 +0200
     1.3 @@ -336,15 +336,17 @@
     1.4  			      [(*filled in specify*)]))
     1.5  
     1.6    | applicable_in (p,p_) pt (Apply_Method mI) =                
     1.7 -  if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  
     1.8 -    then Notappl ((tac2str (Apply_Method mI))^
     1.9 -	   " not for pos "^(pos'2str (p,p_)))
    1.10 -  else let
    1.11 -    val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt p;
    1.12 -    val {where_, ...} = get_pbt pI
    1.13 -    val pres = map (mk_env probl |> subst_atomic) where_
    1.14 -    val ctxt = assoc_thy dI |> ProofContext.init_global 
    1.15 -          |> insert_assumptions pres
    1.16 +      if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  
    1.17 +      then Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
    1.18 +      else
    1.19 +        let
    1.20 +          val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;
    1.21 +          val {where_, ...} = get_pbt pI
    1.22 +          val pres = map (mk_env probl |> subst_atomic) where_
    1.23 +          val ctxt = 
    1.24 +            if is_e_ctxt ctxt
    1.25 +            then assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres
    1.26 +            else ctxt
    1.27      (*TODO.WN110416 here do evalprecond according to fun check_preconds'
    1.28        and then decide on Notappl/Appl accordingly once more.
    1.29        Implement after all tests are running, since this changes