# HG changeset patch
# User wenzelm
# Date 1183475826 -7200
# Node ID 38a304b3fe1e64497ba995b8f293191f2fd2f637
# Parent  438c5d2db4828891e376de60a30738f5b9bd00af
Conjunction.mk_conjunction_balanced;

diff -r 438c5d2db482 -r 38a304b3fe1e src/HOL/Nominal/nominal_inductive.ML
--- 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)