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))