1.1 --- a/src/Doc/IsarRef/ML_Tactic.thy	Thu Feb 28 13:19:25 2013 +0100
     1.2 +++ b/src/Doc/IsarRef/ML_Tactic.thy	Thu Feb 28 13:24:51 2013 +0100
     1.3 @@ -119,7 +119,6 @@
     1.4    \begin{tabular}{lll}
     1.5      @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
     1.6      @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
     1.7 -    @{ML strip_tac}~@{text 1} & @{text "\<approx>"} & @{text "intro strip"} \\
     1.8      @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
     1.9        & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
    1.10        & @{text "\<lless>"} & @{text "clarify"} \\

     2.1 --- a/src/HOL/Bali/Basis.thy	Thu Feb 28 13:19:25 2013 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Thu Feb 28 13:24:51 2013 +0100
     2.3 @@ -9,6 +9,8 @@
     2.4  
     2.5  section "misc"
     2.6  
     2.7 +ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
     2.8 +
     2.9  declare split_if_asm  [split] option.split [split] option.split_asm [split]
    2.10  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    2.11  declare if_weak_cong [cong del] option.weak_case_cong [cong del]

     3.1 --- a/src/HOL/HOL.thy	Thu Feb 28 13:19:25 2013 +0100
     3.2 +++ b/src/HOL/HOL.thy	Thu Feb 28 13:24:51 2013 +0100
     3.3 @@ -1987,8 +1987,6 @@
     3.4  subsection {* Legacy tactics and ML bindings *}
     3.5  
     3.6  ML {*
     3.7 -fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
     3.8 -
     3.9  (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
    3.10  local
    3.11    fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t

     4.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 28 13:19:25 2013 +0100
     4.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 28 13:24:51 2013 +0100
     4.3 @@ -198,7 +198,7 @@
     4.4  
     4.5  -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
     4.6  apply( simp_all)
     4.7 -apply( tactic "ALLGOALS strip_tac")
     4.8 +apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
     4.9  apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
    4.10                   THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
    4.11  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")