# HG changeset patch
# User wenzelm
# Date 1329243537 -3600
# Node ID 4cf5a84e2c055e113a3b471950fd3b16f033bbe6
# Parent  3d0629a9ffca633e4644f735f914535b28e8de8a
normalized aliases;

diff -r 3d0629a9ffca -r 4cf5a84e2c05 src/HOL/Boogie/Tools/boogie_tactics.ML
--- 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)
diff -r 3d0629a9ffca -r 4cf5a84e2c05 src/HOL/Tools/SMT/smt_solver.ML
--- 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)
diff -r 3d0629a9ffca -r 4cf5a84e2c05 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- 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')