mono_Int/Un: proper proof, avoid illegal schematic type vars;
removed obsolete ML bindings;

--- a/src/HOL/Lattices.thy	Sat Sep 01 16:12:50 2007 +0200
+++ b/src/HOL/Lattices.thy	Sat Sep 01 18:17:36 2007 +0200
@@ -513,11 +513,15 @@
 
 lemmas [code func del] = inf_set_eq sup_set_eq
 
-lemmas mono_Int = mono_inf
-  [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq]
+lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+  apply (fold inf_set_eq sup_set_eq)
+  apply (erule mono_inf)
+  done
 
-lemmas mono_Un = mono_sup
-  [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq]
+lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
+  apply (fold inf_set_eq sup_set_eq)
+  apply (erule mono_sup)
+  done
 
 instance set :: (type) complete_lattice
   Inf_set_def: "Inf S \<equiv> \<Inter>S"
@@ -581,9 +585,4 @@
 lemmas inf_aci = inf_ACI
 lemmas sup_aci = sup_ACI
 
-ML {*
-val sup_fun_eq = @{thm sup_fun_eq}
-val sup_bool_eq = @{thm sup_bool_eq}
-*}
-
 end