src/HOL/HOL.thy

   "op &" "HOL.op_and"
   "op |" "HOL.op_or"
   Not "HOL.not"
   arbitrary "HOL.arbitrary"
 
-code_syntax_const
+code_constapp
   "op =" (* an intermediate solution for polymorphic equality *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")
 
 end