--- a/Nominal/nominal_dt_rawperm.ML	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML	Wed Aug 25 09:02:06 2010 +0800
@@ -9,8 +9,8 @@
 
 signature NOMINAL_DT_RAWPERM =
 sig
-  val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory -> 
-    (term list * thm list * thm list) * local_theory
+  val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> 
+    local_theory -> (term list * thm list * thm list) * local_theory
 end
 
 
@@ -90,7 +90,7 @@
 end
 
 
-fun define_raw_perms full_ty_names tys constrs induct_thm lthy =
+fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
 let
   val perm_fn_names = full_ty_names
     |> map Long_Name.base_name
@@ -113,7 +113,7 @@
   val ((perm_funs, perm_eq_thms), lthy') =
     lthy
     |> Local_Theory.exit_global
-    |> Class.instantiation (full_ty_names, [], @{sort pt}) 
+    |> Class.instantiation (full_ty_names, tvs, @{sort pt}) 
     |> Primrec.add_primrec perm_fn_binds perm_eqs
     
   val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'