diff -r 49ab06c0ca64 -r f1980f89c405 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Aug 17 17:52:25 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Tue Aug 17 18:00:55 2010 +0800
@@ -50,7 +50,6 @@
   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
 
@@ -180,10 +179,6 @@
 
 (** function package tactics **)
 
-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)