src/Tools/isac/Interpret/appl.sml
branchdecompose-isar
changeset 41983 4c49adbfadab
parent 41980 6ec461ac6c76
child 41992 1ada058e92bc
     1.1 --- a/src/Tools/isac/Interpret/appl.sml	Wed May 11 14:58:07 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Wed May 11 16:51:30 2011 +0200
     1.3 @@ -619,11 +619,11 @@
     1.4         then (*maybe Apply_Method has already been done*)
     1.5  	 case get_obj g_env pt p of
     1.6  	     SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [], 
     1.7 -					   e_term, [], subpbl domID pblID))
     1.8 +					   e_term, [], e_ctxt, subpbl domID pblID))
     1.9  	   | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.10       else (*somewhere later in the script*)
    1.11         Appl (Subproblem' ((domID, pblID, e_metID), [], 
    1.12 -			  e_term, [], subpbl domID pblID))
    1.13 +			  e_term, [], e_ctxt, subpbl domID pblID))
    1.14  
    1.15    | applicable_in p pt (End_Subproblem) =
    1.16    error ("applicable_in: not impl. for "^