# HG changeset patch
# User paulson
# Date 1231865244 0
# Node ID 0fbfbbec4a92990a75d80e916753ac91a3718649
# Parent  5fc19891652c39ccadead95a19509e3b62bc0aea# Parent  7bae3abff5d7cadc7027c6c71b229b7bcac211e0
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

diff -r 5fc19891652c -r 0fbfbbec4a92 src/HOL/MetisExamples/Abstraction.thy
--- a/src/HOL/MetisExamples/Abstraction.thy	Tue Jan 13 08:20:12 2009 -0800
+++ b/src/HOL/MetisExamples/Abstraction.thy	Tue Jan 13 16:47:24 2009 +0000
@@ -62,9 +62,9 @@
 
 ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect"*}
 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-(*???metis cannot prove this
-by (metis CollectD SigmaD1 SigmaD2 UN_eq)
-Also, UN_eq is unnecessary*)
+(*???metis says this is satisfiable!
+by (metis CollectD SigmaD1 SigmaD2)
+*)
 by (meson CollectD SigmaD1 SigmaD2)
 
 
diff -r 5fc19891652c -r 0fbfbbec4a92 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Jan 13 08:20:12 2009 -0800
+++ b/src/HOL/Tools/res_clause.ML	Tue Jan 13 16:47:24 2009 +0000
@@ -279,6 +279,14 @@
 (*Given a list of sorted type variables, return a list of type literals.*)
 fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts);
 
+(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
+  * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
+    in a lemma has the same sort as 'a in the conjecture.
+  * Deleting such clauses will lead to problems with locales in other use of local results
+    where 'a is fixed. Probably we should delete clauses unless the sorts agree.
+  * Currently we include a class constraint in the clause, exactly as with TVars.
+*)
+
 (** make axiom and conjecture clauses. **)
 
 fun get_tvar_strs [] = []