--- a/Nominal/nominal_dt_supp.ML	Sun Aug 29 01:17:36 2010 +0800
+++ b/Nominal/nominal_dt_supp.ML	Sun Aug 29 01:45:07 2010 +0800
@@ -9,6 +9,9 @@
 sig
   val prove_supports: Proof.context -> thm list -> term list -> thm list  
   val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
+
+  val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
+    local_theory -> local_theory
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -75,5 +78,25 @@
   |> map zero_var_indexes
 end
 
+
+(* finite supp instances *)
+
+fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
+let
+  val lthy1 = 
+    lthy
+    |> Local_Theory.exit_global
+    |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) 
+  
+  fun tac _ =
+    Class.intro_classes_tac [] THEN
+      (ALLGOALS (resolve_tac qfsupp_thms))
+in
+  lthy1
+  |> Class.prove_instantiation_exit tac 
+  |> Named_Target.theory_init
+end
+
+
 end (* structure *)