--- a/Nominal/NewParser.thy	Thu Apr 29 10:11:48 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Apr 29 10:59:08 2010 +0200
@@ -277,7 +277,7 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
@@ -460,11 +460,12 @@
   P1 name
 | P2 pt pt
 binder
- bn::"pt \<Rightarrow> atom set" 
+ bn::"pt \<Rightarrow> atom set"
 where
   "bn (P1 x) = {atom x}"
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
+thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
 
 nominal_datatype exp =
   EVar name