--- a/Nominal-General/nominal_library.ML	Thu May 27 18:40:10 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Mon May 31 19:57:29 2010 +0200
@@ -43,6 +43,12 @@
     (term * typ * typ list * bool list) list
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
+  (* tactics for function package *)
+  val pat_completeness_auto: Proof.context -> tactic
+  val pat_completeness_simp: thm list -> Proof.context -> tactic
+  val prove_termination: Proof.context -> Function.info * local_theory
+
+  
 end
 
 
@@ -150,6 +156,23 @@
 end
 
 
+(** function package **)
+fun pat_completeness_auto lthy =
+  Pat_Completeness.pat_completeness_tac lthy 1
+    THEN auto_tac (clasimpset_of lthy)
+
+fun pat_completeness_simp simps lthy =
+let
+  val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
+in
+  Pat_Completeness.pat_completeness_tac lthy 1
+    THEN ALLGOALS (asm_full_simp_tac simp_set)
+end
+
+fun prove_termination lthy =
+  Function.prove_termination NONE
+    (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file