# HG changeset patch
# User berghofe
# Date 1127990006 -7200
# Node ID 1bdef3df973563abc74382507455f799996676db
# Parent  7efbe0ec9d4c67a0e173eedfd845ddb0445b563a
Simplifier now removes flex-flex constraints from theorem returned by prover.

diff -r 7efbe0ec9d4c -r 1bdef3df9735 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Sep 29 12:30:30 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Sep 29 12:33:26 2005 +0200
@@ -1134,7 +1134,7 @@
    trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ss ct;
    check_bounds ss ct;
    let val {thy, t, maxidx, ...} = Thm.rep_cterm ct
-       val res = bottomc (mode, prover, thy, maxidx) ss ct
+       val res = bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct
          handle THM (s, _, thms) =>
          error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
            Pretty.string_of (Display.pretty_thms thms))