src/HOL/HOL.thy

   ""            :: "case_syn => cases_syn"               ("_")
   "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
 
 translations
   "x ~= y"                == "~ (x = y)"
-  "THE x. P"              => "The (%x. P)"
+  "THE x. P"              == "The (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
 print_translation {*
 (* To avoid eta-contraction of body: *)