src/HOL/Tools/Nitpick/nitpick.ML

   | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
 
 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
 
 val syntactic_sorts =
-  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
   @{sort number}
 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
     subset (op =) (S, syntactic_sorts)
   | has_tfree_syntactic_sort _ = false
 val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)