# HG changeset patch
# User nipkow
# Date 1013684767 -3600
# Node ID f6c1e7306c4099ce8986d95d77b3651d73c24ea5
# Parent  d25b43743e10f6dd7a122b8c26680edd774dbf3f
nodups -> distinct

diff -r d25b43743e10 -r f6c1e7306c40 src/HOL/MicroJava/J/Conform.thy
--- 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")
diff -r d25b43743e10 -r f6c1e7306c40 src/HOL/MicroJava/J/JBasis.thy
--- 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)]: 
diff -r d25b43743e10 -r f6c1e7306c40 src/HOL/MicroJava/J/JTypeSafe.thy
--- 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)
diff -r d25b43743e10 -r f6c1e7306c40 src/HOL/MicroJava/J/WellType.thy
--- 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>