# HG changeset patch
# User haftmann
# Date 1274884135 -7200
# Node ID ee23611b6bf25220a6eaac6c4134ecf4b60b6f2b
# Parent  bac3d00a910a974cb4e8d77a09025109dc0a94b9
dropped legacy theorem bindings

diff -r bac3d00a910a -r ee23611b6bf2 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Wed May 26 16:17:30 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy	Wed May 26 16:28:55 2010 +0200
@@ -189,7 +189,7 @@
 apply     (tactic "ax_tac 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
 apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
+apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
 apply      (tactic "ax_tac 2" (* NewA *))
 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
 apply       (tactic "ax_tac 3")
diff -r bac3d00a910a -r ee23611b6bf2 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:17:30 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:28:55 2010 +0200
@@ -90,7 +90,7 @@
 val before_set2pred_simp_tac =
   (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
 
-val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
+val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]));
 
 (*****************************************************************************)
 (** set2pred_tac transforms sets inclusion into predicates implication,     **)
@@ -111,7 +111,7 @@
     rtac CollectI i,
     dtac CollectD i,
     TRY (split_all_tac i) THEN_MAYBE
-     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
+     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]);
 
 (*****************************************************************************)
 (** BasicSimpTac is called to simplify all verification conditions. It does **)
@@ -125,7 +125,7 @@
 
 fun BasicSimpTac var_names tac =
   simp_tac
-    (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
+    (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
   THEN_MAYBE' MaxSimpTac var_names tac;