diff -r a6319699e517 -r 52971512d1a2 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sun Aug 10 12:38:26 2008 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 11 14:49:53 2008 +0200
@@ -317,13 +317,9 @@
 
 instance inat :: wellorder
 proof
-  show "wf {(x::inat, y::inat). x < y}"
-  proof (rule wfUNIVI)
-    fix P and x :: inat
-    assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
-    hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
-    thus "P x" by (rule inat_less_induct)
-  qed
+  fix P and n
+  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
+  show "P n" by (blast intro: inat_less_induct hyp)
 qed