"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed May 09 22:14:26 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed May 09 23:28:18 2007 +0200
@@ -166,7 +166,7 @@
 val by_pat_completeness_simp =
     Proof.global_terminal_proof
       (Method.Basic (K pat_completeness),
-       SOME (Method.Source_i (Args.src (("HOL.simp_all", []), Position.none))))
+       SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 val termination_by_lexicographic_order =
     FundefPackage.setup_termination_proof NONE