--- a/src/HOL/MicroJava/BV/JVMType.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sat Nov 01 14:20:38 2014 +0100
@@ -363,7 +363,7 @@
theorem sup_state_length [simp]:
"G \<turnstile> s2 <=s s1 \<Longrightarrow>
length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
- by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
+ by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def)
theorem sup_state_append_snd:
"length a = length b \<Longrightarrow>