--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jun 07 20:03:40 2015 +0200
@@ -81,7 +81,7 @@
val ctxt1 =
ctxt
|> Context_Position.not_really
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+ |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
val typs =
map snd type_insts
@@ -144,7 +144,7 @@
let
val ctxt = Context.proof_of context;
val ctxt1 = ctxt
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+ |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
val insts' = insts @ concl_inst;
--- a/src/HOL/Eisbach/match_method.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Sun Jun 07 20:03:40 2015 +0200
@@ -113,7 +113,7 @@
| NONE =>
let
val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
- val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
+ val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
--- a/src/HOL/Eisbach/method_closure.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Sun Jun 07 20:03:40 2015 +0200
@@ -328,7 +328,7 @@
fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
end;
-fun gen_method_definition prep_vars name vars uses attribs methods source lthy =
+fun gen_method_definition prep_var name vars uses attribs methods source lthy =
let
val (uses_nms, lthy1) = lthy
|> Proof_Context.concealed
@@ -339,7 +339,7 @@
|> fold_map setup_local_fact uses;
val ((xs, Ts), lthy2) = lthy1
- |> prep_vars vars |-> Proof_Context.add_fixes
+ |> fold_map prep_var vars |-> Proof_Context.add_fixes
|-> (fn xs => fold_map Proof_Context.inferred_param xs #>> pair xs);
val term_args = map Free (xs ~~ Ts);
@@ -385,8 +385,8 @@
|> add_method name ((term_args', named_thms, method_names), text')
end;
-val method_definition = gen_method_definition Proof_Context.cert_vars;
-val method_definition_cmd = gen_method_definition Proof_Context.read_vars;
+val method_definition = gen_method_definition Proof_Context.cert_var;
+val method_definition_cmd = gen_method_definition Proof_Context.read_var;
val _ =
Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Jun 07 20:03:40 2015 +0200
@@ -736,7 +736,7 @@
fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
let
- val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
+ val (_, ctxt') = Proof_Context.read_var raw_var ctxt
val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
val error_msg = cat_lines
["Lifting failed for the following term:",
@@ -759,7 +759,7 @@
fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
let
val config = evaluate_params params
- val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy
+ val ((binding, SOME qty, mx), lthy) = Proof_Context.read_var raw_var lthy
val var = (binding, mx)
val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
val par_thms = Attrib.eval_thms lthy par_xthms
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Jun 07 20:03:40 2015 +0200
@@ -58,7 +58,7 @@
let
val rty = fastype_of rhs
val qty = fastype_of lhs
- val absrep_trm =
+ val absrep_trm =
Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
val (_, prop') = Local_Defs.cert_def lthy prop
@@ -69,13 +69,13 @@
(* data storage *)
val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
-
+
fun qualify defname suffix = Binding.name suffix
|> Binding.qualify true defname
val lhs_name = Binding.name_of (#1 var)
val rsp_thm_name = qualify lhs_name "rsp"
-
+
val lthy'' = lthy'
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi =>
@@ -83,7 +83,7 @@
qcinfo as {qconst = Const (c, _), ...} =>
Quotient_Info.update_quotconsts (c, qcinfo)
| _ => I))
- |> (snd oo Local_Theory.note)
+ |> (snd oo Local_Theory.note)
((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
in
(qconst_data, lthy'')
@@ -92,14 +92,14 @@
fun mk_readable_rsp_thm_eq tm lthy =
let
val ctm = Thm.cterm_of lthy tm
-
- fun norm_fun_eq ctm =
+
+ fun norm_fun_eq ctm =
let
fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
fun erase_quants ctm' =
case (Thm.term_of ctm') of
Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.all_conv ctm'
- | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
+ | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
in
(abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
@@ -107,52 +107,55 @@
fun simp_arrows_conv ctm =
let
- val unfold_conv = Conv.rewrs_conv
- [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]},
+ val unfold_conv = Conv.rewrs_conv
+ [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]},
@{thm rel_fun_def[THEN eq_reflection]}]
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
case (Thm.term_of ctm) of
- Const (@{const_name rel_fun}, _) $ _ $ _ =>
+ Const (@{const_name rel_fun}, _) $ _ $ _ =>
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => Conv.all_conv ctm
end
- val unfold_ret_val_invs = Conv.bottom_conv
- (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
+ val unfold_ret_val_invs = Conv.bottom_conv
+ (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
val beta_conv = Thm.beta_conversion true
- val eq_thm =
+ val eq_thm =
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
in
Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
end
-
-fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
+fun gen_quotient_def prep_var parse_term (raw_var, (attr, (raw_lhs, raw_rhs))) lthy =
let
- val (vars, ctxt) = prep_vars (the_list raw_var) lthy
- val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
- val lhs = prep_term T_opt ctxt lhs_raw
- val rhs = prep_term NONE ctxt rhs_raw
+ val (opt_var, ctxt) =
+ (case raw_var of
+ NONE => (NONE, lthy)
+ | SOME var => prep_var var lthy |>> SOME)
+ val lhs_constraint = (case opt_var of SOME (_, SOME T, _) => T | _ => dummyT)
+
+ fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
+ val lhs = prep_term lhs_constraint raw_lhs
+ val rhs = prep_term dummyT raw_rhs
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
val _ = if is_Const rhs then () else warning "The definiens is not a constant"
val var =
- (case vars of
- [] => (Binding.name lhs_str, NoSyn)
- | [(binding, _, mx)] =>
+ (case opt_var of
+ NONE => (Binding.name lhs_str, NoSyn)
+ | SOME (binding, _, mx) =>
if Variable.check_name binding = lhs_str then (binding, mx)
- else error_msg binding lhs_str
- | _ => raise Match)
-
- fun try_to_prove_refl thm =
+ else error_msg binding lhs_str);
+
+ fun try_to_prove_refl thm =
let
val lhs_eq =
thm
@@ -167,7 +170,7 @@
| SOME _ => (case body_type (fastype_of lhs) of
Type (typ_name, _) =>
try (fn () =>
- #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
+ #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
RS @{thm Equiv_Relations.equivp_reflp} RS thm) ()
| _ => NONE
)
@@ -179,32 +182,25 @@
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
-
- fun after_qed thm_list lthy =
+
+ fun after_qed thm_list lthy =
let
val internal_rsp_thm =
case thm_list of
[] => the maybe_proven_rsp_thm
- | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
+ | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
in
snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
end
-
in
case maybe_proven_rsp_thm of
SOME _ => Proof.theorem NONE after_qed [] lthy
| NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
end
-fun check_term' cnstr ctxt =
- Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
-
-fun read_term' cnstr ctxt =
- check_term' cnstr ctxt o Syntax.parse_term ctxt
-
-val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
-val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
+val quotient_def = gen_quotient_def Proof_Context.cert_var (K I)
+val quotient_def_cmd = gen_quotient_def Proof_Context.read_var Syntax.parse_term
(* parser and command *)
--- a/src/Pure/Isar/bundle.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Sun Jun 07 20:03:40 2015 +0200
@@ -57,9 +57,9 @@
local
-fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
+fun gen_bundle prep_fact prep_att prep_var (binding, raw_bundle) fixes lthy =
let
- val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
+ val (_, ctxt') = lthy |> fold_map prep_var fixes |-> Proof_Context.add_fixes;
val bundle0 = raw_bundle
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
val bundle =
@@ -75,8 +75,8 @@
in
-val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
-val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
+val bundle = gen_bundle (K I) (K I) Proof_Context.cert_var;
+val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
end;
--- a/src/Pure/Isar/expression.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/expression.ML Sun Jun 07 20:03:40 2015 +0200
@@ -291,11 +291,11 @@
(** Prepare locale elements **)
-fun declare_elem prep_vars (Fixes fixes) ctxt =
- let val (vars, _) = prep_vars fixes ctxt
+fun declare_elem prep_var (Fixes fixes) ctxt =
+ let val (vars, _) = fold_map prep_var fixes ctxt
in ctxt |> Proof_Context.add_fixes vars |> snd end
- | declare_elem prep_vars (Constrains csts) ctxt =
- ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
+ | declare_elem prep_var (Constrains csts) ctxt =
+ ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
| declare_elem _ (Assumes _) ctxt = ctxt
| declare_elem _ (Defines _) ctxt = ctxt
| declare_elem _ (Notes _) ctxt = ctxt;
@@ -358,7 +358,7 @@
local
fun prep_full_context_statement
- parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
+ parse_typ parse_prop prep_var_elem prep_inst prep_var_inst prep_expr
{strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
let
val thy = Proof_Context.theory_of ctxt1;
@@ -384,7 +384,7 @@
let
val ctxt' = ctxt
|> Context_Position.set_visible false
- |> declare_elem prep_vars_elem raw_elem
+ |> declare_elem prep_var_elem raw_elem
|> Context_Position.restore_visible ctxt;
val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
in (elems', ctxt') end;
@@ -394,7 +394,7 @@
val concl = parse_concl parse_prop ctxt raw_concl;
in check_autofix insts elems concl ctxt end;
- val fors = prep_vars_inst fixed ctxt1 |> fst;
+ val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
@@ -426,16 +426,16 @@
in
fun cert_full_context_statement x =
- prep_full_context_statement (K I) (K I) Proof_Context.cert_vars
- make_inst Proof_Context.cert_vars (K I) x;
+ prep_full_context_statement (K I) (K I) Proof_Context.cert_var
+ make_inst Proof_Context.cert_var (K I) x;
fun cert_read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
- make_inst Proof_Context.cert_vars (K I) x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
+ make_inst Proof_Context.cert_var (K I) x;
fun read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
- parse_inst Proof_Context.read_vars check_expr x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
+ parse_inst Proof_Context.read_var check_expr x;
end;
--- a/src/Pure/Isar/obtain.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Sun Jun 07 20:03:40 2015 +0200
@@ -105,7 +105,7 @@
local
-fun gen_obtain prep_att prep_vars prep_propp
+fun gen_obtain prep_att prep_var prep_propp
name raw_vars raw_asms int state =
let
val _ = Proof.assert_forward_or_chain state;
@@ -113,7 +113,7 @@
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
(*obtain vars*)
- val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
+ val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
val xs = map (Variable.check_name o #1) vars;
@@ -163,8 +163,8 @@
in
-val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.read_propp;
+val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.read_propp;
end;
@@ -260,14 +260,16 @@
let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;
-fun gen_guess prep_vars raw_vars int state =
+fun gen_guess prep_var raw_vars int state =
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
- val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
+ val vars = ctxt
+ |> fold_map prep_var raw_vars |-> fold_map inferred_type
+ |> fst |> polymorphic ctxt;
fun guess_context raw_rule state' =
let
@@ -314,8 +316,8 @@
in
-val guess = gen_guess Proof_Context.cert_vars;
-val guess_cmd = gen_guess Proof_Context.read_vars;
+val guess = gen_guess Proof_Context.cert_var;
+val guess_cmd = gen_guess Proof_Context.read_var;
end;
--- a/src/Pure/Isar/proof.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sun Jun 07 20:03:40 2015 +0200
@@ -591,15 +591,15 @@
local
-fun gen_fix prep_vars args =
+fun gen_fix prep_var args =
assert_forward
- #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
+ #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
#> reset_facts;
in
-val fix = gen_fix Proof_Context.cert_vars;
-val fix_cmd = gen_fix Proof_Context.read_vars;
+val fix = gen_fix Proof_Context.cert_var;
+val fix_cmd = gen_fix Proof_Context.read_var;
end;
@@ -630,14 +630,14 @@
local
-fun gen_def prep_att prep_vars prep_binds args state =
+fun gen_def prep_att prep_var prep_binds args state =
let
val _ = assert_forward state;
val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
in
state
- |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
+ |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
|>> map (fn (x, _, mx) => (x, mx))
|-> (fn vars =>
map_context_result (prep_binds false (map swap raw_rhss))
@@ -651,8 +651,8 @@
in
-val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind;
-val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind_cmd;
+val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
+val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Jun 07 20:03:40 2015 +0200
@@ -136,10 +136,10 @@
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
- val read_vars: (binding * string option * mixfix) list -> Proof.context ->
- (binding * typ option * mixfix) list * Proof.context
- val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
- (binding * typ option * mixfix) list * Proof.context
+ val read_var: binding * string option * mixfix -> Proof.context ->
+ (binding * typ option * mixfix) * Proof.context
+ val cert_var: binding * typ option * mixfix -> Proof.context ->
+ (binding * typ option * mixfix) * Proof.context
val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
string list * Proof.context
val add_assms: Assumption.export ->
@@ -1063,21 +1063,20 @@
local
-fun prep_vars prep_typ internal =
- fold_map (fn (b, raw_T, mx) => fn ctxt =>
- let
- val x = check_var internal b;
- fun cond_tvars T =
- if internal then T
- else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
- val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
- val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
- in ((b, opt_T, mx), ctxt') end);
+fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
+ let
+ val x = check_var internal b;
+ fun cond_tvars T =
+ if internal then T
+ else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
+ val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
+ val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
+ in ((b, opt_T, mx), ctxt') end;
in
-val read_vars = prep_vars Syntax.read_typ false;
-val cert_vars = prep_vars (K I) true;
+val read_var = prep_var Syntax.read_typ false;
+val cert_var = prep_var (K I) true;
end;
@@ -1168,7 +1167,7 @@
(* fixes *)
fun add_fixes raw_vars ctxt =
- let val vars = #1 (cert_vars raw_vars ctxt) in
+ let val (vars, _) = fold_map cert_var raw_vars ctxt in
ctxt
|> Variable.add_fixes_binding (map #1 vars)
|-> (fn xs =>
--- a/src/Pure/Isar/specification.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Isar/specification.ML Sun Jun 07 20:03:40 2015 +0200
@@ -87,7 +87,7 @@
fun read_props raw_props raw_fixes ctxt =
let
- val ctxt1 = ctxt |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+ val ctxt1 = ctxt |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
val props1 = map (Syntax.parse_prop ctxt1) raw_props;
val (props2, ctxt2) = ctxt1 |> fold_map Variable.fix_dummy_patterns props1;
val props3 = Syntax.check_props ctxt2 props2;
@@ -130,9 +130,9 @@
in fold_rev close bounds A end;
in map close_form As end;
-fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
+fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
let
- val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
+ val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
val Asss =
@@ -159,23 +159,23 @@
fun single_spec (a, prop) = [(a, [prop])];
fun the_spec (a, [prop]) = (a, prop);
-fun prep_spec prep_vars parse_prop prep_att do_close vars specs =
- prepare prep_vars parse_prop prep_att do_close
+fun prep_spec prep_var parse_prop prep_att do_close vars specs =
+ prepare prep_var parse_prop prep_att do_close
vars (map single_spec specs) #>> apsnd (map the_spec);
in
-fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x;
-fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true x;
+fun check_spec x = prep_spec Proof_Context.cert_var (K I) (K I) true x;
+fun read_spec x = prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src true x;
-fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x;
-fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.check_src false x;
+fun check_free_spec x = prep_spec Proof_Context.cert_var (K I) (K I) false x;
+fun read_free_spec x = prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src false x;
fun check_specification vars specs =
- prepare Proof_Context.cert_vars (K I) (K I) true vars [specs];
+ prepare Proof_Context.cert_var (K I) (K I) true vars [specs];
fun read_specification vars specs =
- prepare Proof_Context.read_vars Syntax.parse_prop Attrib.check_src true vars [specs];
+ prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars [specs];
end;
@@ -309,13 +309,13 @@
local
-fun gen_theorems prep_fact prep_att prep_vars
+fun gen_theorems prep_fact prep_att prep_var
kind raw_facts raw_fixes int lthy =
let
val facts = raw_facts |> map (fn ((name, atts), bs) =>
((name, map (prep_att lthy) atts),
bs |> map (fn (b, more_atts) => (prep_fact lthy b, map (prep_att lthy) more_atts))));
- val (_, ctxt') = lthy |> prep_vars raw_fixes |-> Proof_Context.add_fixes;
+ val (_, ctxt') = lthy |> fold_map prep_var raw_fixes |-> Proof_Context.add_fixes;
val facts' = facts
|> Attrib.partial_evaluation ctxt'
@@ -326,8 +326,8 @@
in
-val theorems = gen_theorems (K I) (K I) Proof_Context.cert_vars;
-val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars;
+val theorems = gen_theorems (K I) (K I) Proof_Context.cert_var;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
end;
--- a/src/Pure/Tools/rule_insts.ML Sun Jun 07 15:35:49 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML Sun Jun 07 20:03:40 2015 +0200
@@ -115,7 +115,7 @@
(*eigen-context*)
val ctxt1 = ctxt
|> Variable.declare_thm thm
- |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+ |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
(*explicit type instantiations*)
val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);