--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Jan 01 13:24:23 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Jan 01 14:29:22 2014 +0100
@@ -227,12 +227,12 @@
in Library.foldr mk_ex (vs, conj) end
val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
(* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
- fun tacs {context = ctxt, prems} = [
+ fun tacs ctxt = [
rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
rtac thm3 1]
in
- val nchotomy = prove thy con_betas goal tacs
+ val nchotomy = prove thy con_betas goal (tacs o #context)
val exhaust =
(nchotomy RS @{thm exh_casedist0})
|> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
@@ -272,8 +272,8 @@
val bottom = mk_bottom (fastype_of v')
val vs' = map (fn v => if v = v' then bottom else v) vs
val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
- val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
in map one_strict nonlazy end
fun con_defin (con, args) =
@@ -286,8 +286,8 @@
val goal = mk_trp (iff_disj (lhs, rhss))
val rule1 = iso_locale RS @{thm iso.abs_bottom_iff}
val rules = rule1 :: @{thms con_bottom_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
in
val con_stricts = maps con_strict spec'
val con_defins = map con_defin spec'
@@ -317,16 +317,16 @@
val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}
val rules2 = @{thms up_defined spair_defined ONE_defined}
val rules = rules1 @ rules2
- val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
- in map (fn c => pgterm mk_below c (K tacs)) cons' end
+ fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
+ in map (fn c => pgterm mk_below c (tacs o #context)) cons' end
val injects =
let
val abs_eq = iso_locale RS @{thm iso.abs_eq}
val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}
val rules2 = @{thms up_defined spair_defined ONE_defined}
val rules = rules1 @ rules2
- val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
- in map (fn c => pgterm mk_eq c (K tacs)) cons' end
+ fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
+ in map (fn c => pgterm mk_eq c (tacs o #context)) cons' end
end
(* prove distinctness of constructors *)
@@ -350,8 +350,8 @@
val goal = mk_trp (iff_disj (lhs, rhss))
val rule1 = iso_locale RS @{thm iso.abs_below}
val rules = rule1 :: @{thms con_below_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
fun dist_eq (con1, args1) (con2, args2) =
let
val (vs1, zs1) = get_vars args1
@@ -362,8 +362,8 @@
val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2))
val rule1 = iso_locale RS @{thm iso.abs_eq}
val rules = rule1 :: @{thms con_eq_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
- in prove thy con_betas goal (K tacs) end
+ fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+ in prove thy con_betas goal (tacs o #context) end
in
val dist_les = map_dist dist_le spec'
val dist_eqs = map_dist dist_eq spec'
@@ -518,8 +518,8 @@
val rules2 = @{thms con_bottom_iff_rules}
val rules3 = @{thms cfcomp2 one_case2}
val rules = abs_inverse :: rules1 @ rules2 @ rules3
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1]
- in prove thy defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]
+ in prove thy defs goal (tacs o #context) end
in
val case_apps = map2 one_case spec fs
end
@@ -586,12 +586,12 @@
val sel_stricts : thm list =
let
val rules = rep_strict :: @{thms sel_strict_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
+ fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
fun sel_strict sel =
let
val goal = mk_trp (mk_strict sel)
in
- prove thy sel_defs goal (K tacs)
+ prove thy sel_defs goal (tacs o #context)
end
in
map sel_strict sel_consts
@@ -602,7 +602,7 @@
let
val defs = con_betas @ sel_defs
val rules = abs_inv :: @{thms sel_app_rules}
- val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
+ fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
let
val Ts : typ list = map #3 args
@@ -617,13 +617,13 @@
val concl = mk_trp (mk_eq (sel ` con_app, nth vs n))
val goal = Logic.list_implies (assms, concl)
in
- prove thy defs goal (K tacs)
+ prove thy defs goal (tacs o #context)
end
fun one_diff (_, sel, T) =
let
val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
in
- prove thy defs goal (K tacs)
+ prove thy defs goal (tacs o #context)
end
fun one_con (j, (_, args')) : thm list =
let
@@ -647,7 +647,7 @@
val sel_defins : thm list =
let
val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules}
- val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
+ fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
fun sel_defin sel =
let
val (T, U) = dest_cfunT (fastype_of sel)
@@ -656,7 +656,7 @@
val rhs = mk_eq (x, mk_bottom T)
val goal = mk_trp (mk_eq (lhs, rhs))
in
- prove thy sel_defs goal (K tacs)
+ prove thy sel_defs goal (tacs o #context)
end
fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
| one_arg _ = NONE
@@ -724,8 +724,8 @@
val assms = map (mk_trp o mk_defined) nonlazy
val concl = mk_trp (mk_eq (lhs, rhs))
val goal = Logic.list_implies (assms, concl)
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
- in prove thy dis_defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+ in prove thy dis_defs goal (tacs o #context) end
fun one_dis (i, dis) =
map_index (dis_app (i, dis)) spec
in
@@ -738,13 +738,13 @@
let
val x = Free ("x", lhsT)
val simps = dis_apps @ @{thms dist_eq_tr}
- val tacs =
+ fun tacs ctxt =
[rtac @{thm iffI} 1,
- asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps dis_stricts) 2,
+ asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps dis_stricts) 2,
rtac exhaust 1, atac 1,
- ALLGOALS (asm_full_simp_tac (Simplifier.global_context thy simple_ss addsimps simps))]
+ ALLGOALS (asm_full_simp_tac (put_simpset simple_ss ctxt addsimps simps))]
val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x))
- in prove thy [] goal (K tacs) end
+ in prove thy [] goal (tacs o #context) end
in
val dis_defins = map dis_defin dis_consts
end
@@ -813,8 +813,8 @@
val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat))
val k = Free ("k", U)
val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V))
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
- in prove thy match_defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+ in prove thy match_defs goal (tacs o #context) end
in
val match_stricts = map match_strict match_consts
end
@@ -832,8 +832,8 @@
val assms = map (mk_trp o mk_defined) nonlazy
val concl = mk_trp (mk_eq (lhs, rhs))
val goal = Logic.list_implies (assms, concl)
- val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
- in prove thy match_defs goal (K tacs) end
+ fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+ in prove thy match_defs goal (tacs o #context) end
fun one_match (i, mat) =
map_index (match_app (i, mat)) spec
in