--- 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