# HG changeset patch
# User blanchet
# Date 1302773044 -7200
# Node ID 8e58cc1390c7ec6b5e86d946ae2665691db4a1dd
# Parent  23bb0784b5d048b6f392bc02739c1fd7bc58ce8c
use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer

diff -r 23bb0784b5d0 -r 8e58cc1390c7 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Quotient.thy	Thu Apr 14 11:24:04 2011 +0200
@@ -647,6 +647,7 @@
   proof (intro conjI allI)
     fix a r s
     show "Abs (R (Eps (Rep a))) = a"
+      using [[metis_new_skolemizer = false]]
       by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
     show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
       by (metis homeier6 equivp[simplified part_equivp_def])