# HG changeset patch
# User wenzelm
# Date 1330609708 -3600
# Node ID 125e49d04cf6cccdf615f474b4a7102d90901989
# Parent  a29006291f2bd16c44307a382bffb9301db33a76
tuned proofs;

diff -r a29006291f2b -r 125e49d04cf6 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 01 14:42:05 2012 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 01 14:48:28 2012 +0100
@@ -28,8 +28,8 @@
   "list_all' P xs \<equiv> list_all'_rec P 0 xs"
 
 lemma list_all'_rec:
-  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
-  apply (induct xs)
+  "list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
+  apply (induct xs arbitrary: n)
   apply auto
   apply (case_tac p)
   apply auto
diff -r a29006291f2b -r 125e49d04cf6 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:42:05 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:48:28 2012 +0100
@@ -127,7 +127,7 @@
 lemma wf_java_mdecl_disjoint_varnames: 
   "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) 
   \<Longrightarrow> disjoint_varnames pns lvars"
-apply (case_tac S)
+apply (cases S)
 apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
 done