--- a/Nominal/Fv.thy	Tue Mar 09 16:57:51 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 09 17:02:29 2010 +0100
@@ -328,7 +328,7 @@
      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
      (add_binds alpha_eqs) [] lthy'')
 in
-  ((fvs, alphas), lthy'')
+  ((fvs, alphas), lthy''')
 end
 *}