src/HOL/MicroJava/J/WellType.thy
changeset 12888 f6c1e7306c40
parent 12517 360e3215f029
child 12911 704713ca07ea
     1.1 --- a/src/HOL/MicroJava/J/WellType.thy	Thu Feb 14 11:50:52 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Thu Feb 14 12:06:07 2002 +0100
     1.3 @@ -209,7 +209,7 @@
     1.4   wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
     1.5  "wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
     1.6    length pTs = length pns \<and>
     1.7 -  nodups pns \<and>
     1.8 +  distinct pns \<and>
     1.9    unique lvars \<and>
    1.10          This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
    1.11    (\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>