# HG changeset patch
# User wenzelm
# Date 1316807509 -7200
# Node ID 3cc2ac688fd971ea6240f1fe117cc2de7edcded1
# Parent  d5156aa8556d04ab001e3770155ff29bd07a54c5
tuned proof;

diff -r d5156aa8556d -r 3cc2ac688fd9 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- 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)"