src/HOL/ex/MT.thy
changeset 42793 88bee9f6eec7
parent 41460 ea56b98aee83
child 51305 4a96f9e28e6d
     1.1 --- a/src/HOL/ex/MT.thy	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/ex/MT.thy	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -869,7 +869,7 @@
     1.4           ve + {ev |-> v} hastyenv te + {ev |=> t}"
     1.5  apply (unfold hasty_env_def)
     1.6  apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
     1.7 -apply (tactic {* safe_tac HOL_cs *})
     1.8 +apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
     1.9  apply (case_tac "ev=x")
    1.10  apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
    1.11  apply (simp add: ve_app_owr2 te_app_owr2)
    1.12 @@ -906,7 +906,7 @@
    1.13      v_clos(cl) hasty t"
    1.14  apply (unfold hasty_env_def hasty_def)
    1.15  apply (drule elab_fix_elim)
    1.16 -apply (tactic {* safe_tac HOL_cs *})
    1.17 +apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
    1.18  (*Do a single unfolding of cl*)
    1.19  apply (frule ssubst) prefer 2 apply assumption
    1.20  apply (rule hasty_rel_clos_coind)
    1.21 @@ -914,7 +914,7 @@
    1.22  apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
    1.23  
    1.24  apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
    1.25 -apply (tactic {* safe_tac HOL_cs *})
    1.26 +apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
    1.27  apply (case_tac "ev2=ev1a")
    1.28  apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
    1.29  apply blast