--- a/Nominal/NewAlpha.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewAlpha.thy	Thu May 20 21:23:53 2010 +0100
@@ -1,7 +1,18 @@
 theory NewAlpha
-imports "NewFv"
+imports "Abs" "Perm" "Nominal2_FSet"
+uses ("nominal_dt_rawperm.ML")
+     ("nominal_dt_rawfuns.ML")
 begin
 
+use "nominal_dt_rawperm.ML"
+use "nominal_dt_rawfuns.ML"
+
+ML {*
+open Nominal_Dt_RawPerm
+open Nominal_Dt_RawFuns
+*}
+
+
 ML {*
 fun mk_binop2 ctxt s (l, r) =
   Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)
@@ -16,17 +27,16 @@
 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
   bn_alphabn alpha_const binds bodys =
 let
-  val thy = ProofContext.theory_of lthy;
-  fun bind_set args (NONE, no) = setify thy (nth args no)
+  fun bind_set args (NONE, no) = setify lthy (nth args no)
     | bind_set args (SOME f, no) = f $ (nth args no)
-  fun bind_lst args (NONE, no) = listify thy (nth args no)
+  fun bind_lst args (NONE, no) = listify lthy (nth args no)
     | bind_lst args (SOME f, no) = f $ (nth args no)
   fun append (t1, t2) =
     Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2;
   fun binds_fn args nos =
     if alpha_const = @{const_name alpha_lst}
     then foldr1 append (map (bind_lst args) nos)
-    else mk_union (map (bind_set args) nos);
+    else fold_union (map (bind_set args) nos);
   val lhs_binds = binds_fn args binds;
   val rhs_binds = binds_fn args2 binds;
   val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);
@@ -64,7 +74,7 @@
 ML {*
 fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm =
 case bm of
-  BEmy i =>
+  BC (_, [], [i]) =>
     let
       val arg = nth args i;
       val arg2 = nth args2 i;
@@ -77,11 +87,11 @@
       | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2]
       | SOME NONE => []
     end
-| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_res} x y
 *}
 
@@ -137,7 +147,7 @@
 ML {*
 fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =
 case bm of
-  BEmy i =>
+  BC (_, [], [i]) =>
     let
       val arg = nth args i;
       val arg2 = nth args2 i;
@@ -147,11 +157,11 @@
       then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
       else [HOLogic.mk_eq (arg, arg2)]
     end
-| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
     fv_frees bn_alphabn @{const_name alpha_res} x y
 *}