--- a/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 23:50:16 2011 +0100
@@ -172,7 +172,7 @@
done
} note this [dest]
- from prems show ?thesis by blast
+ from assms show ?thesis by blast
qed