use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
authorblanchet
Thu Apr 14 11:24:04 2011 +0200 (2011-04-14)
changeset 423348e58cc1390c7
parent 42333 23bb0784b5d0
child 42335 cb8aa792d138
use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -647,6 +647,7 @@
     1.4    proof (intro conjI allI)
     1.5      fix a r s
     1.6      show "Abs (R (Eps (Rep a))) = a"
     1.7 +      using [[metis_new_skolemizer = false]]
     1.8        by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
     1.9      show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
    1.10        by (metis homeier6 equivp[simplified part_equivp_def])