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