src/HOL/Tools/SMT/smt_solver.ML

     ('a * (int option * thm)) list -> int -> 'a smt_filter_data
   val smt_filter_apply: Time.time -> 'a smt_filter_data ->
     {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}
 
   (*tactic*)
-  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
-  val smt_tac': Proof.context -> thm list -> int -> Tactical.tactic
+  val smt_tac: Proof.context -> thm list -> int -> tactic
+  val smt_tac': Proof.context -> thm list -> int -> tactic
 
   (*setup*)
   val setup: theory -> theory
 end
 

 
   fun tag_rules thms = map_index (apsnd (pair NONE)) thms
   fun tag_prems thms = map (pair ~1 o pair NONE) thms
 
   fun resolve (SOME thm) = Tactic.rtac thm 1
-    | resolve NONE = Tactical.no_tac
+    | resolve NONE = no_tac
 
   fun tac prove ctxt rules =
     CONVERSION (SMT_Normalize.atomize_conv ctxt)
     THEN' Tactic.rtac @{thm ccontr}
     THEN' SUBPROOF (fn {context, prems, ...} =>