1.1 --- a/src/HOL/Bali/Basis.thy	Fri Feb 15 20:41:19 2002 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Fri Feb 15 20:41:39 2002 +0100
     1.3 @@ -280,7 +280,7 @@
     1.4  
     1.5  constdefs
     1.6    unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
     1.7 - "unique \<equiv> nodups \<circ> map fst"
     1.8 + "unique \<equiv> distinct \<circ> map fst"
     1.9  
    1.10  lemma uniqueD [rule_format (no_asm)]: 
    1.11  "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"

     2.1 --- a/src/HOL/Bali/Conform.thy	Fri Feb 15 20:41:19 2002 +0100
     2.2 +++ b/src/HOL/Bali/Conform.thy	Fri Feb 15 20:41:39 2002 +0100
     2.3 @@ -205,7 +205,7 @@
     2.4  
     2.5  lemma lconf_ext_list [rule_format (no_asm)]: "
     2.6   \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
     2.7 -      \<forall>vs Ts. nodups vns \<longrightarrow> length Ts = length vns 
     2.8 +      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
     2.9        \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
    2.10  apply (unfold lconf_def)
    2.11  apply (induct_tac "vns")

     3.1 --- a/src/HOL/Bali/WellForm.thy	Fri Feb 15 20:41:19 2002 +0100
     3.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Feb 15 20:41:39 2002 +0100
     3.3 @@ -63,7 +63,7 @@
     3.4   "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
     3.5  			    \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
     3.6                              is_acc_type G P (resTy mh) \<and>
     3.7 -			    \<spacespace> nodups (pars mh)"
     3.8 +			    \<spacespace> distinct (pars mh)"
     3.9  
    3.10  
    3.11  text {*
    3.12 @@ -103,7 +103,7 @@
    3.13  
    3.14  lemma wf_mheadI: 
    3.15  "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
    3.16 -  is_acc_type G P (resTy m); nodups (pars m)\<rbrakk> \<Longrightarrow>  
    3.17 +  is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow>  
    3.18    wf_mhead G P sig m"
    3.19  apply (unfold wf_mhead_def)
    3.20  apply (simp (no_asm_simp))