--- a/src/HOL/MicroJava/J/Conform.thy Thu Feb 14 11:50:52 2002 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Thu Feb 14 12:06:07 2002 +0100
@@ -238,7 +238,7 @@
done
lemma lconf_ext_list [rule_format (no_asm)]:
- "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. nodups vns --> length Ts = length vns -->
+ "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns --> length Ts = length vns -->
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)"
apply (unfold lconf_def)
apply( induct_tac "vns")
--- a/src/HOL/MicroJava/J/JBasis.thy Thu Feb 14 11:50:52 2002 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Thu Feb 14 12:06:07 2002 +0100
@@ -14,7 +14,7 @@
constdefs
unique :: "('a \<times> 'b) list => bool"
- "unique == nodups \<circ> map fst"
+ "unique == distinct \<circ> map fst"
lemma fst_in_set_lemma [rule_format (no_asm)]:
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 14 11:50:52 2002 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 14 12:06:07 2002 +0100
@@ -93,7 +93,7 @@
lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;
- length pTs' = length pns; nodups pns;
+ length pTs' = length pns; distinct pns;
Ball (set lvars) (split (\<lambda>vn. is_type G))
|] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
apply (unfold wf_mhead_def)
--- 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>