src/HOL/ex/Records.thy

--- a/src/HOL/ex/Records.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/ex/Records.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -254,37 +254,40 @@
 *}
 
 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1 *})
+  apply (tactic {* simp_tac (put_simpset HOL_basic_ss @{context}
+    addsimprocs [Record.split_simproc (K ~1)]) 1 *})
   apply simp
   done
 
 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
   apply simp
   done
 
 lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1 *})
+  apply (tactic {* simp_tac (put_simpset HOL_basic_ss @{context}
+    addsimprocs [Record.split_simproc (K ~1)]) 1 *})
   apply simp
   done
 
 lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1 *})
+  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1 *})
   apply simp
   done
 
 lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1 *})
+  apply (tactic {* simp_tac (put_simpset HOL_basic_ss @{context}
+    addsimprocs [Record.split_simproc (K ~1)]) 1 *})
   apply auto
   done
 
 lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
   apply auto
   done
 
 lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
   apply auto
   done
 
@@ -295,7 +298,7 @@
     assume pre: "P (xpos r)"
     then have "\<exists>x. P x"
       apply -
-      apply (tactic {* Record.split_simp_tac [] (K ~1) 1 *})
+      apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1 *})
       apply auto
       done
   }
@@ -306,7 +309,8 @@
   illustrated by the following lemma. *}
 
 lemma "\<exists>r. xpos r = x"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1 *})
+  apply (tactic {* simp_tac (put_simpset HOL_basic_ss @{context}
+    addsimprocs [Record.ex_sel_eq_simproc]) 1 *})
   done