--- a/src/HOL/Tools/Function/function_core.ML Wed May 29 16:12:05 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed May 29 18:25:11 2013 +0200
@@ -351,7 +351,8 @@
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
+ Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+ |> Seq.list_of |> the_single
val uniqueness = G_cases
|> Thm.forall_elim (cterm_of thy lhs)