src/HOL/Bali/Conform.thy
changeset 12893 cbb4dc5e6478
parent 12858 6214f03d6d27
child 12925 99131847fb93
--- 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")