# HG changeset patch
# User krauss
# Date 1271857533 -7200
# Node ID fd95c0514623697953720560f1ab60c492e9d528
# Parent  fa30cbb455df6036aec8a62835d82f2222dadbd1
tolerate eta-variants in f_graph.cases (from inductive package); added test case;

diff -r fa30cbb455df -r fd95c0514623 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Apr 21 15:37:39 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Apr 21 15:45:33 2010 +0200
@@ -349,12 +349,15 @@
     val unique_clauses =
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
 
+    fun elim_implies_eta A AB =
+      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
+
     val uniqueness = G_cases
       |> forall_elim (cterm_of thy lhs)
       |> forall_elim (cterm_of thy y)
       |> forall_elim P
       |> Thm.elim_implies G_lhs_y
-      |> fold Thm.elim_implies unique_clauses
+      |> fold elim_implies_eta unique_clauses
       |> implies_intr (cprop_of G_lhs_y)
       |> forall_intr (cterm_of thy y)
 
diff -r fa30cbb455df -r fd95c0514623 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Wed Apr 21 15:37:39 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Wed Apr 21 15:45:33 2010 +0200
@@ -290,6 +290,14 @@
   "tinc (Leaf n) = Leaf (Suc n)"
 | "tinc (Branch l) = Branch (map tinc l)"
 
+fun testcase :: "'a tree \<Rightarrow> 'a list"
+where
+  "testcase (Leaf a) = [a]"
+| "testcase (Branch x) =
+    (let xs = concat (map testcase x);
+         ys = concat (map testcase x) in
+     xs @ ys)"
+
 
 (* Pattern matching on records *)
 record point =