src/HOL/UNITY/UNITY.ML

--- a/src/HOL/UNITY/UNITY.ML	Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Fri Aug 30 16:42:45 2002 +0200
@@ -131,12 +131,6 @@
 
 (*** co ***)
 
-(*These operators are not overloaded, but their operands are sets, and 
-  ultimately there's a risk of reaching equality, which IS overloaded*)
-overload_1st_set "UNITY.constrains";
-overload_1st_set "UNITY.stable";
-overload_1st_set "UNITY.unless";
-
 val prems = Goalw [constrains_def]
     "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
 \    ==> F : A co A'";