Simplifier now removes flex-flex constraints from theorem returned by prover.

--- 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))