--- a/src/HOL/HOLCF/Tools/cpodef.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun Nov 09 20:41:53 2014 +0100
@@ -15,14 +15,14 @@
Rep_bottom_iff: thm, Abs_bottom_iff: thm }
val add_podef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic -> theory ->
+ term -> (binding * binding) option -> (Proof.context -> tactic) -> theory ->
(Typedef.info * thm) * theory
val add_cpodef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic * tactic -> theory ->
- (Typedef.info * cpo_info) * theory
+ term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
+ theory -> (Typedef.info * cpo_info) * theory
val add_pcpodef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic * tactic -> theory ->
- (Typedef.info * cpo_info * pcpo_info) * theory
+ term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
+ theory -> (Typedef.info * cpo_info * pcpo_info) * theory
val cpodef_proof:
(binding * (string * sort) list * mixfix) * term
@@ -205,7 +205,7 @@
fun cpodef_result nonempty admissible thy =
let
val ((info as (_, {type_definition, ...}), below_def), thy) = thy
- |> add_podef typ set opt_morphs (rtac nonempty 1)
+ |> add_podef typ set opt_morphs (fn _ => rtac nonempty 1)
val (cpo_info, thy) = thy
|> prove_cpo name newT morphs type_definition below_def admissible
in
@@ -237,7 +237,7 @@
fun pcpodef_result bottom_mem admissible thy =
let
- val tac = rtac exI 1 THEN rtac bottom_mem 1
+ fun tac _ = rtac exI 1 THEN rtac bottom_mem 1
val ((info as (_, {type_definition, ...}), below_def), thy) = thy
|> add_podef typ set opt_morphs tac
val (cpo_info, thy) = thy
@@ -260,10 +260,10 @@
let
val (goal1, goal2, cpodef_result) =
prepare_cpodef Syntax.check_term typ set opt_morphs thy
- val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+ val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context)
handle ERROR msg => cat_error msg
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
- val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+ val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context)
handle ERROR msg => cat_error msg
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set))
in cpodef_result thm1 thm2 thy end
@@ -272,10 +272,10 @@
let
val (goal1, goal2, pcpodef_result) =
prepare_pcpodef Syntax.check_term typ set opt_morphs thy
- val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+ val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context)
handle ERROR msg => cat_error msg
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
- val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+ val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context)
handle ERROR msg => cat_error msg
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set))
in pcpodef_result thm1 thm2 thy end
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Nov 09 20:41:53 2014 +0100
@@ -108,8 +108,8 @@
val set = @{term "defl_set :: udom defl => udom set"} $ defl
(*pcpodef*)
- val tac1 = rtac @{thm defl_set_bottom} 1
- val tac2 = rtac @{thm adm_defl_set} 1
+ fun tac1 _ = rtac @{thm defl_set_bottom} 1
+ fun tac2 _ = rtac @{thm adm_defl_set} 1
val ((info, cpo_info, pcpo_info), thy) = thy
|> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2)
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 20:41:53 2014 +0100
@@ -578,7 +578,7 @@
(name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
(Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
- (rtac exI 1 THEN rtac CollectI 1 THEN
+ (fn _ => rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
let
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 09 20:41:53 2014 +0100
@@ -770,7 +770,7 @@
val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
- (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val repTB = mk_T_of_bnf Ds Bs bnf;
val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
@@ -800,7 +800,7 @@
val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
maybe_typedef false (bdT_bind, params, NoSyn)
- (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ (HOLogic.mk_UNIV bd_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl},
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 09 20:41:53 2014 +0100
@@ -719,7 +719,7 @@
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
typedef (sbdT_bind, sum_bdT_params', NoSyn)
- (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ (HOLogic.mk_UNIV sum_bdT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val sbdT = Type (sbdT_name, sum_bdT_params);
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
@@ -1269,7 +1269,7 @@
lthy
|> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final =>
typedef (b, params, mx) car_final NONE
- (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
+ (fn _ => EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
|>> apsnd split_list o split_list;
val Ts = map (fn name => Type (name, params')) T_names;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 09 20:41:53 2014 +0100
@@ -457,7 +457,7 @@
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
typedef (sbdT_bind, sum_bdT_params', NoSyn)
- (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ (HOLogic.mk_UNIV sum_bdT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val sbdT = Type (sbdT_name, sum_bdT_params);
val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
@@ -716,7 +716,7 @@
val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
typedef (IIT_bind, params, NoSyn)
- (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ (HOLogic.mk_UNIV II_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val IIT = Type (IIT_name, params');
val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
@@ -860,7 +860,7 @@
lthy
|> @{fold_map 3} (fn b => fn mx => fn car_init =>
typedef (b, params, mx) car_init NONE
- (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
+ (fn _ => EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
rtac alg_init_thm] 1)) bs mixfixes car_inits
|>> apsnd split_list o split_list;
@@ -1393,7 +1393,7 @@
val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
- (HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ (HOLogic.mk_UNIV sum_bd0T) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val sbd0T = Type (sbd0T_name, sum_bd0T_params);
val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
--- a/src/HOL/Tools/BNF/bnf_util.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Sun Nov 09 20:41:53 2014 +0100
@@ -104,7 +104,8 @@
val parse_map_rel_bindings: (binding * binding) parser
val typedef: binding * (string * sort) list * mixfix -> term ->
- (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
+ (binding * binding) option -> (Proof.context -> tactic) ->
+ local_theory -> (string * Typedef.info) * local_theory
end;
structure BNF_Util : BNF_UTIL =
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 20:41:53 2014 +0100
@@ -188,7 +188,7 @@
(fn (((name, mx), tvs), c) =>
Typedef.add_typedef_global false (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
- (rtac exI 1 THEN rtac CollectI 1 THEN
+ (fn _ => rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac rep_intrs 1)))
(types_syntax ~~ tyvars ~~ take (length newTs) rep_set_names)
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sun Nov 09 20:41:53 2014 +0100
@@ -42,7 +42,7 @@
(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
let
- val typedef_tac =
+ fun typedef_tac _ =
EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
in
Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
--- a/src/HOL/Tools/record.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/record.ML Sun Nov 09 20:41:53 2014 +0100
@@ -112,7 +112,7 @@
in
thy
|> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
- (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
+ (HOLogic.mk_UNIV repT) NONE (fn _ => rtac UNIV_witness 1)
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
--- a/src/HOL/Tools/typedef.ML Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/typedef.ML Sun Nov 09 20:41:53 2014 +0100
@@ -17,9 +17,11 @@
val get_info_global: theory -> string -> info list
val interpretation: (string -> local_theory -> local_theory) -> theory -> theory
val add_typedef: bool -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
+ term -> (binding * binding) option -> (Proof.context -> tactic) -> local_theory ->
+ (string * info) * local_theory
val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
+ term -> (binding * binding) option -> (Proof.context -> tactic) -> theory ->
+ (string * info) * theory
val typedef: (binding * (string * sort) list * mixfix) * term *
(binding * binding) option -> local_theory -> Proof.state
val typedef_cmd: (binding * (string * string option) list * mixfix) * string *
@@ -245,7 +247,7 @@
val ((goal, _, typedef_result), lthy') =
prepare_typedef conceal Syntax.check_term typ set opt_morphs lthy;
val inhabited =
- Goal.prove lthy' [] [] goal (K tac)
+ Goal.prove lthy' [] [] goal (tac o #context)
|> Goal.norm_result lthy' |> Thm.close_derivation;
in typedef_result inhabited lthy' end;