src/HOL/MicroJava/J/JTypeSafe.thy
changeset 12888 f6c1e7306c40
parent 12517 360e3215f029
child 12911 704713ca07ea
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 14 11:50:52 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 14 12:06:07 2002 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4  
     1.5  lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;  
     1.6     list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
     1.7 -  length pTs' = length pns; nodups pns;  
     1.8 +  length pTs' = length pns; distinct pns;  
     1.9    Ball (set lvars) (split (\<lambda>vn. is_type G))  
    1.10    |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
    1.11  apply (unfold wf_mhead_def)