--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Tue Feb 14 17:54:08 2012 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Tue Feb 14 19:18:57 2012 +0100
@@ -92,7 +92,7 @@
(Rule_Cases.make_common
(Proof_Context.theory_of ctxt,
Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names))
- Tactical.all_tac st))
+ all_tac st))
in
val setup_boogie_cases = Method.setup @{binding boogie_cases}
(Scan.succeed boogie_cases)
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 14 17:54:08 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Feb 14 19:18:57 2012 +0100
@@ -39,8 +39,8 @@
{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
@@ -357,7 +357,7 @@
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)
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Feb 14 17:54:08 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Feb 14 19:18:57 2012 +0100
@@ -724,14 +724,14 @@
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
@@ -740,7 +740,7 @@
Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
(fn ctxt' =>
Z3_Proof_Tools.by_tac (
- (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+ (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')