src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/HOL.thy	Fri Aug 30 16:42:45 2002 +0200
@@ -603,13 +603,6 @@
   "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
   "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
 
-(*Tell blast about overloading of < and <= to reduce the risk of
-  its applying a rule for the wrong type*)
-ML {*
-Blast.overloaded ("op <" , domain_type);
-Blast.overloaded ("op <=", domain_type);
-*}
-
 
 subsubsection {* Monotonicity *}