equal
deleted
inserted
replaced
37 |
37 |
38 consts |
38 consts |
39 exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list" |
39 exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list" |
40 primrec |
40 primrec |
41 "exec_mr Return stk0 frs = |
41 "exec_mr Return stk0 frs = |
42 (let val = hd stk0; (stk,loc,cn,met,pc) = hd frs |
42 (if frs=[] then [] |
43 in |
43 else let val = hd stk0; (stk,loc,cn,met,pc) = hd frs |
44 (val#stk,loc,cn,met,pc)#tl frs)" |
44 in (val#stk,loc,cn,met,pc)#tl frs)" |
45 |
45 |
46 end |
46 end |