diff -r 1e6160690546 -r 107c06267f33 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Aug 15 11:03:13 2010 +0800
@@ -10,6 +10,8 @@
 
   val dest_listT: typ -> typ
 
+  val size_const: typ -> term 
+
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -73,13 +75,15 @@
 fun dest_listT (Type (@{type_name list}, [T])) = T
   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
 
-fun mk_minus p = @{term "uminus::perm => perm"} $ p;
+fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
 
-fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;
+fun mk_minus p = @{term "uminus::perm => perm"} $ p
 
-fun perm_ty ty = @{typ "perm"} --> ty --> ty; 
-fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm;
-fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm;
+fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
+
+fun perm_ty ty = @{typ "perm"} --> ty --> ty
+fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t]);