diff -r f1522b892a4c -r 5a176b8dda84 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'";