1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Thu Feb 14 11:50:52 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Thu Feb 14 12:06:07 2002 +0100
     1.3 @@ -238,7 +238,7 @@
     1.4  done
     1.5  
     1.6  lemma lconf_ext_list [rule_format (no_asm)]: 
     1.7 -  "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. nodups vns --> length Ts = length vns --> 
     1.8 +  "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns --> length Ts = length vns --> 
     1.9    list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
    1.10  apply (unfold lconf_def)
    1.11  apply( induct_tac "vns")

     2.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Thu Feb 14 11:50:52 2002 +0100
     2.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Thu Feb 14 12:06:07 2002 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4   
     2.5  constdefs
     2.6    unique  :: "('a \<times> 'b) list => bool"
     2.7 -  "unique  == nodups \<circ> map fst"
     2.8 +  "unique  == distinct \<circ> map fst"
     2.9  
    2.10  
    2.11  lemma fst_in_set_lemma [rule_format (no_asm)]: 

     3.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 14 11:50:52 2002 +0100
     3.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 14 12:06:07 2002 +0100
     3.3 @@ -93,7 +93,7 @@
     3.4  
     3.5  lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;  
     3.6     list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
     3.7 -  length pTs' = length pns; nodups pns;  
     3.8 +  length pTs' = length pns; distinct pns;  
     3.9    Ball (set lvars) (split (\<lambda>vn. is_type G))  
    3.10    |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
    3.11  apply (unfold wf_mhead_def)

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