diff -r d7d4491535a9 -r 3c4eff4a73da Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Tue May 18 11:45:49 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Tue May 18 11:46:19 2010 +0200
@@ -27,7 +27,7 @@
 
 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
 
-local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *}
+local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *}
 lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*)
 
 lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"