# HG changeset patch
# User blanchet
# Date 1277137936 -7200
# Node ID b993fac7985b638aad84ca5892128e0df2ac9bb3
# Parent  4de0b0c38bdfa1fb6f0ebd3fcb45f94c305776e7
beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later;
reintroduced old proof based on Metis, since it was a good test for the Skolemizer

diff -r 4de0b0c38bdf -r b993fac7985b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 21 16:59:37 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 21 18:32:16 2010 +0200
@@ -5266,7 +5266,7 @@
     (* class constraint due to continuous_on_inverse *)
   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
           \<Longrightarrow> s homeomorphic t"
-  unfolding homeomorphic_def by (auto intro: homeomorphism_compact)
+  unfolding homeomorphic_def by (metis homeomorphism_compact)
 
 text{* Preservation of topological properties.                                   *}
 
diff -r 4de0b0c38bdf -r b993fac7985b src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 21 16:59:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 21 18:32:16 2010 +0200
@@ -137,7 +137,7 @@
 
 fun mk_skolem_id t =
   let val T = fastype_of t in
-    Const (@{const_name skolem_id}, T --> T) $ Envir.beta_eta_contract t
+    Const (@{const_name skolem_id}, T --> T) $ Envir.beta_norm t
   end
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
@@ -446,7 +446,7 @@
 
 (**** Translate a set of theorems into CNF ****)
 
-fun pair_name_cls k (n, []) = []
+fun pair_name_cls _ (_, []) = []
   | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
 
 (*The combination of rev and tail recursion preserves the original order*)