Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Conjunction.mk_conjunction_balanced;
authorwenzelm
Tue, 03 Jul 2007 17:17:06 +0200
changeset 23531 38a304b3fe1e
parent 23530 438c5d2db482
child 23532 802bdbe08177
Conjunction.mk_conjunction_balanced;
src/HOL/Nominal/nominal_inductive.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jul 03 17:17:04 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jul 03 17:17:06 2007 +0200
@@ -243,8 +243,8 @@
                    let
                      val th' = gprems1 MRS
                        Thm.instantiate (Thm.first_order_match
-                         (Conjunction.mk_conjunction_list (cprems_of th),
-                          Conjunction.mk_conjunction_list (map cprop_of gprems1))) th;
+                         (Conjunction.mk_conjunction_balanced (cprems_of th),
+                          Conjunction.mk_conjunction_balanced (map cprop_of gprems1))) th;
                      val (bop, lhs, rhs) = (case concl_of th' of
                          _ $ (fresh $ lhs $ rhs) =>
                            (fn t => fn u => fresh $ t $ u, lhs, rhs)
isabelle