diff -r 1577cbcd0936 -r 2b97bd6415b7 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri Jun 24 13:01:53 1994 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 29 12:01:17 1994 +0200
@@ -311,7 +311,7 @@
 
     fun constrain T =
       Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC, 
-            [max_pri, 0], max_pri - 1)
+            [4, 0], 3)
 
     fun unhide T =
       if T <> logicT then