diff -r abada9e6f943 -r 953f74f40727 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Fri Apr 30 10:04:24 2010 +0200
+++ b/Nominal/NewFv.thy	Fri Apr 30 10:31:32 2010 +0200
@@ -281,7 +281,7 @@
   val fv_bns_exp = map (Morphism.term morphism) fv_bns
 
 in
-  ((fv_frees_exp, fv_bns_exp), info, lthy'')
+  ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'')
 end
 *}