diff -r a2f70c09e77d -r 95aac598a526 Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Mon May 17 16:25:45 2010 +0100
+++ b/Nominal/Manual/Term4.thy	Mon May 17 17:54:07 2010 +0100
@@ -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))"