src/HOL/Boogie/Tools/boogie_loader.ML

             (case AList.lookup (op =) atts "unique" of
               SOME _ => Symtab.lookup fds name
             | NONE => NONE)
         | is_unique _ = NONE
       fun mk_unique_axiom T ts =
-        Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
+        Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
           HOLogic.mk_list T ts
     in
       map_filter is_unique fns
       |> map (swap o Term.dest_Const)
       |> AList.group (op =)

     | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
 
   fun mk_list T = HOLogic.mk_list T
 
   fun mk_distinct T ts =
-    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
+    Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
       mk_list T ts
 
   fun quant name f = scan_line name (num -- num -- num) >> pair f
   val quants =
     quant "forall" HOLogic.all_const ||