src/HOL/Bali/WellForm.thy
changeset 12893 cbb4dc5e6478
parent 12858 6214f03d6d27
child 12925 99131847fb93
     1.1 --- a/src/HOL/Bali/WellForm.thy	Fri Feb 15 20:41:19 2002 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Feb 15 20:41:39 2002 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4   "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
     1.5  			    \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
     1.6                              is_acc_type G P (resTy mh) \<and>
     1.7 -			    \<spacespace> nodups (pars mh)"
     1.8 +			    \<spacespace> distinct (pars mh)"
     1.9  
    1.10  
    1.11  text {*
    1.12 @@ -103,7 +103,7 @@
    1.13  
    1.14  lemma wf_mheadI: 
    1.15  "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
    1.16 -  is_acc_type G P (resTy m); nodups (pars m)\<rbrakk> \<Longrightarrow>  
    1.17 +  is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow>  
    1.18    wf_mhead G P sig m"
    1.19  apply (unfold wf_mhead_def)
    1.20  apply (simp (no_asm_simp))