src/HOLCF/Lift3.ML

 	(res_inst_tac [("f","Iup")] arg_cong  1),
 	(rtac lub_equal 1),
 	(atac 1),
 	(rtac (monofun_Ilift2 RS ch2ch_monofun) 1),
 	(etac (monofun_Iup RS ch2ch_monofun) 1),
-	(asm_simp_tac Lift_ss 1)
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "cont_Iup" Lift3.thy "cont(Iup)"
  (fn prems =>
 	[

 	(rtac trans 1),
 	(rtac (thelub_fun RS sym) 2),
 	(etac (monofun_Ilift1 RS ch2ch_monofun) 2),
 	(rtac ext 1),
 	(res_inst_tac [("p","x")] liftE 1),
-	(asm_simp_tac Lift_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(asm_simp_tac Lift_ss 1),
+	(Asm_simp_tac 1),
 	(etac contlub_cfun_fun 1)
 	]);
 
 
 qed_goal "contlub_Ilift2" Lift3.thy "contlub(Ilift(f))"

 	(strip_tac 1),
 	(rtac disjE 1),
 	(rtac (thelub_lift1a RS ssubst) 2),
 	(atac 2),
 	(atac 2),
-	(asm_simp_tac Lift_ss 2),
+	(Asm_simp_tac 2),
 	(rtac (thelub_lift1b RS ssubst) 3),
 	(atac 3),
 	(atac 3),
 	(fast_tac HOL_cs 1),
-	(asm_simp_tac Lift_ss 2),
+	(Asm_simp_tac 2),
 	(rtac (chain_UU_I_inverse RS sym) 2),
 	(rtac allI 2),
 	(res_inst_tac [("p","Y(i)")] liftE 2),
-	(asm_simp_tac Lift_ss 2),
+	(Asm_simp_tac 2),
 	(rtac notE 2),
 	(dtac spec 2),
 	(etac spec 2),
 	(atac 2),
 	(rtac (contlub_cfun_arg RS ssubst) 1),

 	(atac 1),
 	(rtac defined_Iup2 1),
 	(rtac exI 1),
 	(strip_tac 1),
 	(res_inst_tac [("p","Y(i)")] liftE 1),
-	(asm_simp_tac Lift_ss 2),
+	(Asm_simp_tac 2),
 	(res_inst_tac [("P","Y(i) = UU")] notE 1),
 	(fast_tac HOL_cs 1),
 	(rtac (inst_lift_pcpo RS ssubst) 1),
 	(atac 1)
 	]);

 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up`x)"
  (fn prems =>
 	[
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+	(simp_tac (!simpset addsimps [cont_Iup]) 1),
 	(rtac (inst_lift_pcpo RS ssubst) 1),
 	(rtac Exh_Lift 1)
 	]);
 
 qed_goalw "inject_up" Lift3.thy [up_def] "up`x=up`y ==> x=y"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac inject_Iup 1),
 	(etac box_equals 1),
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+	(simp_tac (!simpset addsimps [cont_Iup]) 1),
+	(simp_tac (!simpset addsimps [cont_Iup]) 1)
 	]);
 
 qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU"
  (fn prems =>
 	[
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+	(simp_tac (!simpset addsimps [cont_Iup]) 1),
 	(rtac defined_Iup2 1)
 	]);
 
 qed_goalw "liftE1" Lift3.thy [up_def] 
 	"[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"

 	[
 	(rtac liftE 1),
 	(resolve_tac prems 1),
 	(etac (inst_lift_pcpo RS ssubst) 1),
 	(resolve_tac (tl prems) 1),
-	(asm_simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Iup]) 1)
 	]);
 
 
 qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift`f`UU=UU"
  (fn prems =>

 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
 		cont_Ilift2,cont2cont_CF1L]) 1)),
 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
 		cont_Ilift2,cont2cont_CF1L]) 1)),
-	(simp_tac (Lift_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
+	(simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
 	]);
 
 qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
  (fn prems =>
 	[

 	(rtac (beta_cfun RS ssubst) 1),
 	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
 		cont_Ilift2,cont2cont_CF1L]) 1)),
 	(rtac (beta_cfun RS ssubst) 1),
 	(rtac cont_Ilift2 1),
-	(simp_tac (Lift_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
+	(simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
 	]);
 
 qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU"
  (fn prems =>
 	[
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+	(simp_tac (!simpset addsimps [cont_Iup]) 1),
 	(rtac less_lift3b 1)
 	]);
 
 qed_goalw "less_lift4c" Lift3.thy [up_def,lift_def]
 	 "(up`x << up`y) = (x<<y)"
  (fn prems =>
 	[
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+	(simp_tac (!simpset addsimps [cont_Iup]) 1),
 	(rtac less_lift2c 1)
 	]);
 
 qed_goalw "thelub_lift2a" Lift3.thy [up_def,lift_def] 
 "[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\

 	(etac exE 1),
 	(rtac exI 1),
 	(rtac exI 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+	(simp_tac (!simpset addsimps [cont_Iup]) 1)
 	]);
 
 
 
 qed_goalw "thelub_lift2b" Lift3.thy [up_def,lift_def] 

 	(rtac swap 1),
 	(atac 1),
 	(dtac notnotD 1),
 	(etac box_equals 1),
 	(rtac refl 1),
-	(simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+	(simp_tac (!simpset addsimps [cont_Iup]) 1)
 	]);
 
 
 qed_goal "lift_lemma2" Lift3.thy  " (? x.z = up`x) = (z~=UU)"
  (fn prems =>

 
 qed_goal "lift3" Lift3.thy "lift`up`x=x"
  (fn prems =>
 	[
 	(res_inst_tac [("p","x")] liftE1 1),
-	(asm_simp_tac (Cfun_ss addsimps [lift1,lift2]) 1),
-	(asm_simp_tac (Cfun_ss addsimps [lift1,lift2]) 1)
+	(asm_simp_tac (!simpset addsimps [lift1,lift2]) 1),
+	(asm_simp_tac (!simpset addsimps [lift1,lift2]) 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
 (* install simplifier for ('a)u                                             *)
 (* ------------------------------------------------------------------------ *)