# HG changeset patch
# User wenzelm
# Date 1013802099 -3600
# Node ID cbb4dc5e64788db0978ed78722190aeeaf87d9c4
# Parent  a0b2acb7d6fac5db882bb452c0f5d94c001234d3
replaced nodups by distinct;

diff -r a0b2acb7d6fa -r cbb4dc5e6478 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Fri Feb 15 20:41:19 2002 +0100
+++ b/src/HOL/Bali/Basis.thy	Fri Feb 15 20:41:39 2002 +0100
@@ -280,7 +280,7 @@
 
 constdefs
   unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
- "unique \<equiv> nodups \<circ> map fst"
+ "unique \<equiv> distinct \<circ> map fst"
 
 lemma uniqueD [rule_format (no_asm)]: 
 "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
diff -r a0b2acb7d6fa -r cbb4dc5e6478 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Fri Feb 15 20:41:19 2002 +0100
+++ b/src/HOL/Bali/Conform.thy	Fri Feb 15 20:41:39 2002 +0100
@@ -205,7 +205,7 @@
 
 lemma lconf_ext_list [rule_format (no_asm)]: "
  \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
-      \<forall>vs Ts. nodups vns \<longrightarrow> length Ts = length vns 
+      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
 apply (unfold lconf_def)
 apply (induct_tac "vns")
diff -r a0b2acb7d6fa -r cbb4dc5e6478 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Fri Feb 15 20:41:19 2002 +0100
+++ b/src/HOL/Bali/WellForm.thy	Fri Feb 15 20:41:39 2002 +0100
@@ -63,7 +63,7 @@
  "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
 			    \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
                             is_acc_type G P (resTy mh) \<and>
-			    \<spacespace> nodups (pars mh)"
+			    \<spacespace> distinct (pars mh)"
 
 
 text {*
@@ -103,7 +103,7 @@
 
 lemma wf_mheadI: 
 "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
-  is_acc_type G P (resTy m); nodups (pars m)\<rbrakk> \<Longrightarrow>  
+  is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow>  
   wf_mhead G P sig m"
 apply (unfold wf_mhead_def)
 apply (simp (no_asm_simp))