1.1 --- a/src/Tools/isac/Interpret/generate.sml	Fri May 20 14:08:14 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri May 20 14:49:07 2011 +0200
     1.3 @@ -441,8 +441,8 @@
     1.4        val pos' = ((lev_on o lev_dn) p, Frm)
     1.5    in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
     1.6  
     1.7 -  | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
     1.8 -      let val (pt,c) = append_result pt p l (scval, map str2term asm) Complete
     1.9 +  | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =
    1.10 +      let val (pt,c) = append_result pt p l (scval, asm) Complete
    1.11        in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), 
    1.12  				   Nundef, term2str scval)), pt) end
    1.13