| 5377 |      1 | consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list
 | 
|  |      2 | primrec
 | 
|  |      3 | "exec s vs [] = vs"
 | 
|  |      4 | "exec s vs (i#is) = (case i of
 | 
|  |      5 |     Const v  => exec s (v#vs) is
 | 
|  |      6 |   | Load a   => exec s ((s a)#vs) is
 | 
|  |      7 |   | Apply f  => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"
 |