Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_function_core.ML
changeset 3219 e5d9b6bca88c
parent 3218 89158f401b07
child 3220 87dbeba4b25a 
--- a/Nominal/nominal_function_core.ML	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jun 04 09:39:23 2013 +0100
@@ -501,8 +501,9 @@
       map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
 
     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)
       |> Thm.forall_elim (cterm_of thy y)
nominal2