# HG changeset patch
# User wenzelm
# Date 1252354412 -7200
# Node ID f97a1e5c9a5a06ee11b52b2d038c8c28f4a0a7c7
# Parent  86035c5f61b56d8174e5ae391da433514b7a0341# Parent  668052c4220e48c3a2286625b597533a4cab9d49
merged

diff -r 668052c4220e -r f97a1e5c9a5a src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 07 22:12:16 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Sep 07 22:13:32 2009 +0200
@@ -68,7 +68,10 @@
    @post v subset s & p(v) &
          forall e in v. ~p(v \ e)
    *)
-  fun minimal p s = min p [] s
+  fun minimal p s =
+    case min p [] s of
+      [x] => if p [] then [] else [x]
+    | m => m
 end