diff -r 4223770814ef -r 47e2e91705f3 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Apr 27 14:30:44 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Apr 27 19:01:22 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Equivp" "Rsp" "Lift"
+        "Perm" "NewFv"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -51,14 +51,6 @@
 *}
 
 ML {*
-datatype bmodes =
-   BEmy of int
-|  BLst of ((term option * int) list) * (int list)
-|  BSet of ((term option * int) list) * (int list)
-|  BRes of ((term option * int) list) * (int list)
-*}
-
-ML {*
 fun get_cnstrs dts =
   map (fn (_, _, _, constrs) => constrs) dts
 
@@ -277,8 +269,17 @@
 
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+
+  val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
+  fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
+  val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
+  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
+  val thy = Local_Theory.exit_global lthy2;
+  val lthy3 = Theory_Target.init NONE thy;
+
+  val (_, lthy4) = define_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
 *}
 
@@ -500,6 +501,7 @@
 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
+thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps