src/HOL/Bali/TypeRel.thy

--- a/src/HOL/Bali/TypeRel.thy	Sun Jul 29 14:29:51 2007 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Sun Jul 29 14:29:52 2007 +0200
@@ -373,7 +373,7 @@
 done
 
 lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K"
-apply (erule make_imp, erule implmt.induct)
+apply (erule rev_mp, erule implmt.induct)
 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
 done