author | wenzelm |
Fri, 23 Sep 2011 21:51:49 +0200 | |
changeset 45068 | 3cc2ac688fd9 |
parent 45067 | d5156aa8556d |
child 45069 | 981098cdbb3f |
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Sep 23 17:35:06 2011 +0200 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Sep 23 21:51:49 2011 +0200 @@ -347,7 +347,7 @@ from some_handler xp' have state': "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)" - by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta + by (cases "ins!pc") (auto simp add: raise_system_xcpt_def split_beta split: split_if_asm) (* takes long! *) let ?f' = "([xcp], loc, C, sig, handler)"