equal
deleted
inserted
replaced
63 \\<Rightarrow> (xcpt option \\<times> opstack \\<times> p_count)" |
63 \\<Rightarrow> (xcpt option \\<times> opstack \\<times> p_count)" |
64 |
64 |
65 primrec |
65 primrec |
66 "exec_ch (Checkcast C) G hp stk pc = |
66 "exec_ch (Checkcast C) G hp stk pc = |
67 (let oref = hd stk; |
67 (let oref = hd stk; |
68 xp' = raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast; |
68 xp' = raise_xcpt (\\<not> cast_ok G (ClassT C) hp oref) ClassCast; |
69 stk' = if xp'=None then stk else tl stk |
69 stk' = if xp'=None then stk else tl stk |
70 in |
70 in |
71 (xp' , stk' , pc+1))" |
71 (xp' , stk' , pc+1))" |
72 |
72 |
73 end |
73 end |