# HG changeset patch
# User krauss
# Date 1178746098 -7200
# Node ID 5ea718c681233d5f1e3ac932f9490dd40555a643
# Parent  38ae2815989f0c3b3ae2193e6d8c039e6eaa561f
"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"

diff -r 38ae2815989f -r 5ea718c68123 src/HOL/Tools/function_package/fundef_datatype.ML
--- 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