# HG changeset patch
# User blanchet
# Date 1277138710 -7200
# Node ID 3da1e49459ee7280edd52be80b271ce374b41bd6
# Parent  64b0356d0f19bb01912793c12088b89d649bac5f# Parent  b993fac7985b638aad84ca5892128e0df2ac9bb3
merged

diff -r 64b0356d0f19 -r 3da1e49459ee src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 21 18:31:52 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 21 18:45:10 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 64b0356d0f19 -r 3da1e49459ee src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 21 18:31:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 21 18:45:10 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*)