1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 09:12:40 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 13:43:25 2011 +0200
     1.3 @@ -1541,7 +1541,7 @@
     1.4                (case par_pbl_det pt p of
     1.5  	               (true, p', _) => 
     1.6  	                  let val (_,pblID,_) = get_obj g_spec pt p';
     1.7 -	                  in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])), 
     1.8 +	                  in (Check_Postcond' (pblID, (v, [(*WN030608 NO asms???*)])), 
     1.9  	                    (e_istate, ctxt), (v,s)) 
    1.10                      end
    1.11  	             | (_, p', rls') => 
    1.12 @@ -1590,7 +1590,7 @@
    1.13       val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
    1.14       val {pre, prls, ...} = get_met metID;
    1.15       val pres = check_preconds thy prls pre itms |> map snd;
    1.16 -     (*val ctxt = ctxt |> insert_assumptions pres;*)
    1.17 +     val ctxt = ctxt |> insert_assumptions pres;
    1.18     in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
    1.19  
    1.20  (* decide, where to get script/istate from: