1.1 --- a/src/Tools/isac/Interpret/generate.sml	Fri May 20 09:12:40 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri May 20 13:43:25 2011 +0200
     1.3 @@ -442,10 +442,8 @@
     1.4    in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
     1.5  
     1.6    | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
     1.7 -    let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
     1.8 -       (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
     1.9 -	val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
    1.10 -    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), 
    1.11 +      let val (pt,c) = append_result pt p l (scval, (*map str2term asm*)[]) Complete
    1.12 +      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), 
    1.13  				   Nundef, term2str scval)), pt) end
    1.14  
    1.15    | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =