diff -r 29532d69111c -r b51532dd5689 Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Fri Jun 18 15:22:58 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Wed Jun 23 08:48:38 2010 +0200
@@ -42,7 +42,7 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
 lemmas alpha_inj = alpha4_inj(1-3)
 
-lemma alpha_fix: "alpha_rtrm4_list = list_rel alpha_rtrm4"
+lemma alpha_fix: "alpha_rtrm4_list = list_all2 alpha_rtrm4"
   apply (rule ext)+
   apply (induct_tac x xa rule: list_induct2')
   apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
@@ -105,7 +105,7 @@
   (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
 
 lemma [quot_respect]:
-  "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
+  "(alpha_rtrm4 ===> list_all2 alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
   by (simp add: alpha_inj_fixed)
 
 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
@@ -126,7 +126,7 @@
   apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified])
   done
 
-lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute"
+lemma [quot_respect]: "(op = ===> list_all2 alpha_rtrm4 ===> list_all2 alpha_rtrm4) permute permute"
   apply simp
   apply (rule allI)+
   apply (induct_tac xa y rule: list_induct2')