src/Tools/isac/Interpret/appl.sml
branchdecompose-isar
changeset 41948 023ebb7d9759
parent 41933 8d38adf87848
child 41952 0e76e17a430a
     1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sat Mar 19 15:18:10 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Mon Mar 21 00:32:53 2011 +0100
     1.3 @@ -343,7 +343,7 @@
     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*)))
     1.8 +  else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), e_ctxt))
     1.9  
    1.10    | applicable_in (p,p_) pt (Check_Postcond pI) =
    1.11    if member op = [Pbl,Met] p_