src/HOL/Library/Tools/smt_word.ML

 
   fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
   fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
 
   fun add_word_fun f (t, n) =
-    let val (m, _) = Term.dest_Const t
+    let val m = dest_Const_name t
     in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
 
   val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
 
   fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t