# HG changeset patch
# User blanchet
# Date 1357918256 -3600
# Node ID 91e6836bb68bf9f79ef311212a78b34b483e4d48
# Parent  aba769dc82e9f3c15fb7b2b29fc6b141cf8f2b34
don't learn from the proof of "psimps" etc.

diff -r aba769dc82e9 -r 91e6836bb68b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 11 16:30:56 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 11 16:30:56 2013 +0100
@@ -622,6 +622,11 @@
    exclusively to "someI_e" (and to some internal constructions). *)
 val class_some_dep = nickname_of_thm @{thm someI_ex}
 
+val fundef_ths =
+  @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff
+         fundef_default_value}
+  |> map nickname_of_thm
+
 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
 val typedef_ths =
   @{thms type_definition.Abs_inverse type_definition.Rep_inverse
@@ -648,8 +653,11 @@
   let
     val deps = thms_in_proof (SOME name_tabs) th
   in
-    if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
-       exists (member (op =) typedef_ths) deps orelse is_size_def deps th then
+    if deps = [typedef_dep] orelse
+       deps = [class_some_dep] orelse
+       exists (member (op =) fundef_ths) deps orelse
+       exists (member (op =) typedef_ths) deps orelse
+       is_size_def deps th then
       []
     else
       deps