diff -r 1378b654acde -r ed280ad05133 thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Thu Mar 06 13:28:38 2014 +0000
+++ b/thys/Hoare_tm.thy	Thu Mar 06 15:28:20 2014 +0000
@@ -954,12 +954,10 @@
 
 lemma listsum_upd_suc:
   "a < length ks \<Longrightarrow> listsum (map Suc (ks[a := Suc (ks ! a)]))= (Suc (listsum (map Suc ks)))"
-by (smt Ex_list_of_length Skolem_list_nth elem_le_listsum_nat 
-     length_induct length_list_update length_map length_splice 
-     list_eq_iff_nth_eq list_ext_get_upd list_ext_lt_get list_update_beyond 
-     list_update_id list_update_overwrite list_update_same_conv list_update_swap 
-     listsum_update_nat map_eq_imp_length_eq map_update neq_if_length_neq 
-     nth_equalityI nth_list_update nth_list_update_eq nth_list_update_neq nth_map reps_sep_len_def)
+by (smt elem_le_listsum_nat 
+     length_list_update list_ext_get_upd 
+     list_update_overwrite listsum_update_nat map_update 
+     nth_equalityI nth_list_update nth_map)
 
 lemma reps_len_suc:
   assumes "a < length ks"
@@ -1915,8 +1913,10 @@
 
   fun atomic tac  = ((SOLVED' tac) ORELSE' (K all_tac))
 
+  fun map_simpset f = Context.proof_map (Simplifier.map_ss f)
+
   fun pure_sep_conj_ac_tac ctxt = 
-         (auto_tac (ctxt |> Simplifier.map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}))
+         (auto_tac (map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}) ctxt)
           |> SELECT_GOAL)
 
 
@@ -1928,7 +1928,7 @@
                                       (pure_sep_conj_ac_tac ctxt i));
 
   fun sep_conj_ac_tac ctxt = 
-     (SOLVED' (auto_tac (ctxt |> Simplifier.map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}))
+     (SOLVED' (auto_tac (ctxt |> map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}))
        |> SELECT_GOAL)) ORELSE' (atomic (some_fact_tac ctxt))
 *}
 
@@ -2339,7 +2339,7 @@
                (if conclusion then (orig, reordered) else (reordered, orig));
   val rule =
    Goal.prove ctxt [] [] goal (fn _ => 
-        auto_tac (ctxt |> Simplifier.map_simpset (fn ss => ss addsimps @{thms sep_conj_ac})))
+        auto_tac (ctxt |> map_simpset (fn ss => ss addsimps @{thms sep_conj_ac})))
          |> Drule.export_without_context
 in
    rule