--- 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. *}
--- 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*)