src/HOL/Tools/Nunchaku/nunchaku.ML

   | str_of_mode Try = "Try"
   | str_of_mode Normal = "Normal";
 
 fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns;
 
-fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true
+fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close> $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
   | has_lonely_bool_var _ = false;
 
 val syntactic_sorts =
   \<^sort>\<open>{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}\<close> @ \<^sort>\<open>numeral\<close>;