src/HOL/Tools/SMT/smt_translate.ML

     and in_form t =
       (case Term.strip_comb t of
         (q as Const (qn, _), [Abs (n, T, t')]) =>
           if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
           else as_term (in_term t)
-      | (Const (c as (@{const_name distinct}, T)), [t']) =>
+      | (Const (c as (@{const_name SMT.distinct}, T)), [t']) =>
           if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
           else as_term (in_term t)
       | (Const c, ts) =>
           if is_builtin_conn (conn c)
           then Term.list_comb (Const (conn c), map in_form ts)

               trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
           | NONE => raise TERM ("intermediate", [t]))
       | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
           transT T ##>> trans t1 ##>> trans t2 #>>
           (fn ((U, u1), u2) => SLet (U, u1, u2))
-      | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
+      | (h as Const (c as (@{const_name SMT.distinct}, T)), [t1]) =>
           (case builtin_fun ctxt c (HOLogic.dest_list t1) of
             SOME (n, ts) => fold_map trans ts #>> app n
           | NONE => transs h T [t1])
       | (h as Const (c as (_, T)), ts) =>
           (case try HOLogic.dest_number t of