src/Pure/Syntax/syn_ext.ML

     fun mkvar T =
       Mfix ("_", varT --> change_name T "_A", "", [], max_pri);
 
     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
         [Mfix ("_", change_name T "_H" --> T, "", [0], 0),
          Mfix ("_", change_name T "_A" --> T, "", [0], 0)]