--- a/Nominal-General/nominal_library.ML	Mon Apr 19 15:37:54 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Mon Apr 19 16:55:36 2010 +0200
@@ -7,6 +7,8 @@
 signature NOMINAL_LIBRARY =
 sig
   val mk_minus: term -> term
+  val mk_plus: term -> term -> term
+
   val mk_perm_ty: typ -> term -> term -> term
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
@@ -20,7 +22,10 @@
 struct
 
 fun mk_minus p = 
- Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
+ @{term "uminus::perm => perm"} $ p
+
+fun mk_plus p q =
+ @{term "plus::perm => perm => perm"} $ p $ q
 
 fun mk_perm_ty ty p trm =
   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm

--- a/Nominal/Fv.thy	Mon Apr 19 15:37:54 2010 +0200
+++ b/Nominal/Fv.thy	Mon Apr 19 16:55:36 2010 +0200
@@ -274,7 +274,6 @@
 end;
 *}
 
-ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
 ML {*
 fun non_rec_binds l =
@@ -596,7 +595,7 @@
                 val fv = mk_compound_fv fvs;
                 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
                 val alpha = mk_compound_alpha alphas;
-                val pi = foldr1 add_perm (distinct (op =) rpis);
+                val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis);
                 val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
                 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
               in
@@ -618,7 +617,7 @@
               val rhs = mk_pair (rhs_binds, arg2);
               val alpha = nth alpha_frees (body_index dt);
               val fv = nth fv_frees (body_index dt);
-              val pi = foldr1 add_perm (distinct (op =) rpis);
+              val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis);
               val alpha_const = alpha_const_for_binds rbinds;
               val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre

--- a/Nominal/Perm.thy	Mon Apr 19 15:37:54 2010 +0200
+++ b/Nominal/Perm.thy	Mon Apr 19 16:55:36 2010 +0200
@@ -3,11 +3,6 @@
 begin
 
 ML {*
-  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
-  open Nominal_Library; 
-*}
-
-ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
 let
   val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
@@ -26,54 +21,53 @@
   val perm_types = map fastype_of perm_frees;
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
   fun glc ((perm, T), x) =
-    HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T))
+    HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T))
   val gl =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
       (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
   fun tac _ =
     EVERY [
-      indtac induct perm_indnames 1,
+      Datatype_Aux.indtac induct perm_indnames 1,
       ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
     ];
 in
-  split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
+  Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
 end;
 *}
 
 ML {*
 fun prove_perm_append lthy induct perm_def perm_frees =
 let
-  val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
   val pi1 = Free ("pi1", @{typ perm});
   val pi2 = Free ("pi2", @{typ perm});
   val perm_types = map fastype_of perm_frees
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
   fun glc ((perm, T), x) =
     HOLogic.mk_eq (
-      perm $ (add_perm $ pi1 $ pi2) $ Free (x, T),
+      perm $ (mk_plus pi1 pi2) $ Free (x, T),
       perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
-  val gl =
+  val goal =
     (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
       (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
   fun tac _ =
     EVERY [
-      indtac induct perm_indnames 1,
+      Datatype_Aux.indtac induct perm_indnames 1,
       ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
     ]
 in
-  split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac)
+  Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac)
 end;
 *}
 
 ML {*
-fun define_raw_perms (dt_info : info) number thy =
+fun define_raw_perms (dt_info : Datatype_Aux.info) number thy =
 let
   val {descr, induct, sorts, ...} = dt_info;
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val full_tnames = List.take (all_full_tnames, number);
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i);
   val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
-    "permute_" ^ name_of_typ (nth_dtyp i)) descr);
+    "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
   val perm_types = map (fn (i, _) =>
     let val T = nth_dtyp i
     in @{typ perm} --> T --> T end) descr;
@@ -81,17 +75,17 @@
   val pi = Free ("pi", @{typ perm});
   fun perm_eq_constr i (cname, dts) =
     let
-      val Ts = map (typ_of_dtyp descr sorts) dts;
+      val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
       val args = map Free (names ~~ Ts);
       val c = Const (cname, Ts ---> (nth_dtyp i));
       fun perm_arg (dt, x) =
         let val T = type_of x
         in
-          if is_rec_type dt then
+          if Datatype_Aux.is_rec_type dt then
             let val (Us, _) = strip_type T
             in list_abs (map (pair "x") Us,
-              Free (nth perm_names_types' (body_index dt)) $ pi $
+              Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
                 list_comb (x, map (fn (i, U) =>
                   (mk_perm_ty U (mk_minus pi) (Bound i)))
                   ((length Us - 1 downto 0) ~~ Us)))
@@ -180,18 +174,18 @@
 (* Test
 atom_decl name
 
-datatype rtrm1 =
-  rVr1 "name"
-| rAp1 "rtrm1" "rtrm1 list"
-| rLm1 "name" "rtrm1"
-| rLt1 "bp" "rtrm1" "rtrm1"
+datatype trm =
+  Var "name"
+| App "trm" "trm list"
+| Lam "name" "trm"
+| Let "bp" "trm" "trm"
 and bp =
   BUnit
-| BVr "name"
-| BPr "bp" "bp"
+| BVar "name"
+| BPair "bp" "bp"
 
 
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}
+setup {* snd o define_raw_perms ["trm", "bp"] ["Perm.trm", "Perm.bp"] *}
 print_theorems
 *)