src/HOL/ex/Records.thy

 equations for simplification and can also split fixed record variables.
 
 *}
 
 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
 
 lemma True
 proof -
   {
     fix P r
     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
   }
   show ?thesis ..
 qed
 
 text {* The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is
   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
 
 
 subsection {* A more complex record expression *}