--- a/Quot/Nominal/Fv.thy	Wed Feb 17 15:28:50 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 15:45:03 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "Nominal2_Atoms"
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -27,6 +27,7 @@
 
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
+  (* TODO: It is the same as one in 'nominal_atoms' *)
   fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
   val noatoms = @{term "{} :: atom set"};
   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
@@ -41,35 +42,13 @@
     HOLogic.mk_binop @{const_name minus} (a, b);
 *}
 
-atom_decl name
-
-datatype rtrm1 =
-  rVr1 "name"
-| rAp1 "rtrm1" "rtrm1"
-| rLm1 "name" "rtrm1"        --"name is bound in trm1"
-| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
-and bp =
-  BUnit
-| BVr "name"
-| BPr "bp" "bp"
-
-(* to be given by the user *)
-
-primrec 
-  bv1
-where
-  "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-
-ML maps
 ML {*
-  val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1";
-  val sorts = [];
-  val bindsall = [
-    [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
-    [[], [[]], [[], []]]
-  ];
+(* Currently needs just one full_tname to access Datatype *)
+fun define_raw_fv full_tname bindsall lthy =
+let
+  val thy = ProofContext.theory_of lthy
+  val {descr, ...} = Datatype.the_info thy full_tname;
+  val sorts = []; (* TODO *)
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
@@ -106,14 +85,37 @@
     end;
   fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
   val fv_eqs = flat (map2 fv_eq descr bindsall)
+in
+  snd (Primrec.add_primrec
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
+end
 *}
 
 
-local_setup {*
-snd o (Primrec.add_primrec
-  (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs)
-*}
+atom_decl name
+
+datatype rtrm1 =
+  rVr1 "name"
+| rAp1 "rtrm1" "rtrm1"
+| rLm1 "name" "rtrm1"        --"name is bound in trm1"
+| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
+and bp =
+  BUnit
+| BVr "name"
+| BPr "bp" "bp"
+
+(* to be given by the user *)
+
+primrec 
+  bv1
+where
+  "bv1 (BUnit) = {}"
+| "bv1 (BVr x) = {atom x}"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+
+local_setup {* define_raw_fv "Fv.rtrm1"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+   [[], [[]], [[], []]]] *}
 print_theorems
 
-
 end