--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Dec 14 17:28:05 2013 +0100
@@ -157,10 +157,10 @@
(* prove applied version of definitions *)
fun prove_proj (lhs, rhs) =
let
- val tac = rewrite_goals_tac fixdef_thms THEN
+ fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
(simp_tac (Simplifier.global_context thy beta_ss)) 1
val goal = Logic.mk_equals (lhs, rhs)
- in Goal.prove_global thy [] [] goal (K tac) end
+ in Goal.prove_global thy [] [] goal (tac o #context) end
val proj_thms = map prove_proj projs
(* mk_tuple lhss == fixpoint *)
@@ -328,7 +328,7 @@
in
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
EVERY
- [rewrite_goals_tac map_apply_thms,
+ [rewrite_goals_tac ctxt map_apply_thms,
rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
REPEAT (resolve_tac adm_rules 1),
simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
@@ -533,11 +533,11 @@
let
val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
val DEFL_simps = RepData.get (Proof_Context.init_global thy)
- val tac =
- rewrite_goals_tac (map mk_meta_eq DEFL_simps)
+ fun tac ctxt =
+ rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
THEN TRY (resolve_tac defl_unfold_thms 1)
in
- Goal.prove_global thy [] [] goal (K tac)
+ Goal.prove_global thy [] [] goal (tac o #context)
end
val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns
@@ -641,7 +641,7 @@
in
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
EVERY
- [rewrite_goals_tac (defl_apply_thms @ map_apply_thms),
+ [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
rtac (@{thm cont_parallel_fix_ind}
OF [defl_cont_thm, map_cont_thm]) 1,
REPEAT (resolve_tac adm_rules 1),