--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jun 14 15:53:13 2015 +0200
@@ -81,7 +81,7 @@
val ctxt1 =
ctxt
|> Context_Position.not_really
- |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
+ |> Proof_Context.add_fixes_cmd fixes |> #2;
val typs =
map snd type_insts
@@ -140,11 +140,10 @@
val inst = Args.maybe Parse_Tools.name_term;
val concl = Args.$$$ "concl" -- Args.colon;
-fun close_unchecked_insts context ((insts,concl_inst), fixes) =
+fun close_unchecked_insts context ((insts, concl_inst), fixes) =
let
val ctxt = Context.proof_of context;
- val ctxt1 = ctxt
- |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
+ val ctxt1 = ctxt |> Proof_Context.add_fixes_cmd fixes |> #2;
val insts' = insts @ concl_inst;
--- a/src/HOL/Eisbach/match_method.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Sun Jun 14 15:53:13 2015 +0200
@@ -112,11 +112,10 @@
| SOME _ => error "Unexpected token value in match cartouche"
| NONE =>
let
- val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
- val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
- val (fix_names, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
-
- val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
+ val (fix_names, ctxt3) = ctxt
+ |> Proof_Context.add_fixes_cmd
+ (map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes)
+ ||> Proof_Context.set_mode Proof_Context.mode_schematic;
fun parse_term term =
if prop_match match_kind
--- a/src/HOL/Eisbach/method_closure.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Sun Jun 14 15:53:13 2015 +0200
@@ -328,7 +328,7 @@
fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
end;
-fun gen_method_definition prep_var name vars uses attribs methods source lthy =
+fun gen_method_definition add_fixes name vars uses attribs methods source lthy =
let
val (uses_nms, lthy1) = lthy
|> Proof_Context.concealed
@@ -339,8 +339,7 @@
|> fold_map setup_local_fact uses;
val (term_args, lthy2) = lthy1
- |> fold_map prep_var vars |-> Proof_Context.add_fixes
- |-> fold_map Proof_Context.inferred_param |>> map Free;
+ |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
val (named_thms, modifiers) = map (check_attrib lthy2) (attribs @ uses) |> split_list;
val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
@@ -384,8 +383,8 @@
|> add_method name ((term_args', named_thms, method_names), text')
end;
-val method_definition = gen_method_definition Proof_Context.cert_var;
-val method_definition_cmd = gen_method_definition Proof_Context.read_var;
+val method_definition = gen_method_definition Proof_Context.add_fixes;
+val method_definition_cmd = gen_method_definition Proof_Context.add_fixes_cmd;
val _ =
Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
--- a/src/Pure/Isar/bundle.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Sun Jun 14 15:53:13 2015 +0200
@@ -57,9 +57,9 @@
local
-fun gen_bundle prep_fact prep_att prep_var (binding, raw_bundle) fixes lthy =
+fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
let
- val (_, ctxt') = lthy |> fold_map prep_var fixes |-> Proof_Context.add_fixes;
+ val (_, ctxt') = add_fixes raw_fixes lthy;
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_var;
-val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
+val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes;
+val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
end;
--- a/src/Pure/Isar/proof.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sun Jun 14 15:53:13 2015 +0200
@@ -594,15 +594,15 @@
local
-fun gen_fix prep_var args =
+fun gen_fix add_fixes raw_fixes =
assert_forward
- #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
+ #> map_context (snd o add_fixes raw_fixes)
#> reset_facts;
in
-val fix = gen_fix Proof_Context.cert_var;
-val fix_cmd = gen_fix Proof_Context.read_var;
+val fix = gen_fix Proof_Context.add_fixes;
+val fix_cmd = gen_fix Proof_Context.add_fixes_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Jun 14 15:53:13 2015 +0200
@@ -131,6 +131,8 @@
(binding * typ option * mixfix) * Proof.context
val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
string list * Proof.context
+ val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context ->
+ string list * Proof.context
val add_assms: Assumption.export ->
(Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
@@ -1131,16 +1133,26 @@
(* fixes *)
-fun add_fixes raw_vars ctxt =
- let val (vars, _) = fold_map cert_var raw_vars ctxt in
- ctxt
- |> Variable.add_fixes_binding (map #1 vars)
- |-> (fn xs =>
- fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
- #-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
- #> pair xs)
+local
+
+fun gen_fixes prep_var raw_vars ctxt =
+ let
+ val (vars, _) = fold_map prep_var raw_vars ctxt;
+ val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
+ in
+ ctxt'
+ |> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
+ |-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
+ |> pair xs
end;
+in
+
+val add_fixes = gen_fixes cert_var;
+val add_fixes_cmd = gen_fixes read_var;
+
+end;
+
(** assumptions **)
--- a/src/Pure/Isar/specification.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Isar/specification.ML Sun Jun 14 15:53:13 2015 +0200
@@ -87,7 +87,7 @@
fun read_props raw_props raw_fixes ctxt =
let
- val ctxt1 = ctxt |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
+ val (_, ctxt1) = ctxt |> Proof_Context.add_fixes_cmd raw_fixes;
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;
@@ -291,13 +291,13 @@
local
-fun gen_theorems prep_fact prep_att prep_var
+fun gen_theorems prep_fact prep_att add_fixes
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 |> fold_map prep_var raw_fixes |-> Proof_Context.add_fixes;
+ val (_, ctxt') = add_fixes raw_fixes lthy;
val facts' = facts
|> Attrib.partial_evaluation ctxt'
@@ -308,8 +308,8 @@
in
-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;
+val theorems = gen_theorems (K I) (K I) Proof_Context.add_fixes;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
end;
--- a/src/Pure/Tools/rule_insts.ML Sun Jun 14 14:59:39 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML Sun Jun 14 15:53:13 2015 +0200
@@ -113,9 +113,9 @@
val vars = Thm.fold_terms Term.add_vars thm [];
(*eigen-context*)
- val ctxt1 = ctxt
+ val (_, ctxt1) = ctxt
|> Variable.declare_thm thm
- |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
+ |> Proof_Context.add_fixes_cmd raw_fixes;
(*explicit type instantiations*)
val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);