src/HOL/Tools/Nunchaku/nunchaku.ML

 
 fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true
   | has_lonely_bool_var _ = false;
 
 val syntactic_sorts =
-  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ @{sort numeral};
+  \<^sort>\<open>{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}\<close> @ \<^sort>\<open>numeral\<close>;
 
 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);