src/Tools/isac/Interpret/generate.sml
branchdecompose-isar
changeset 42017 ce19769e9dc4
parent 42016 ddd4c6d8b439
child 42018 11cf93cd02c6
     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