1.1 --- a/src/Tools/isac/Interpret/generate.sml Fri May 20 13:43:25 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri May 20 14:08:14 2011 +0200
1.3 @@ -442,7 +442,7 @@
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 (pt,c) = append_result pt p l (scval, (*map str2term asm*)[]) Complete
1.8 + let val (pt,c) = append_result pt p l (scval, map str2term asm) Complete
1.9 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
1.10 Nundef, term2str scval)), pt) end
1.11