diff -r 87d98857d154 -r 16464c3f86bd src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Fri Aug 28 20:18:33 2009 +0200
@@ -375,7 +375,7 @@
     hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") 
       by auto
     hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" 
-      by (auto simp add: min_def)
+      by (auto)
     hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" 
       by blast
     hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" 
@@ -391,7 +391,7 @@
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp simp add: min_def)
+  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
   ultimately
   show ?thesis by (rule iffI) 
 qed