--- a/src/HOL/MicroJava/J/WellType.thy Thu Feb 14 11:50:52 2002 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Feb 14 12:06:07 2002 +0100
@@ -209,7 +209,7 @@
wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
length pTs = length pns \<and>
- nodups pns \<and>
+ distinct pns \<and>
unique lvars \<and>
This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>
(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>