--- a/src/Pure/Isar/element.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/element.ML Sun Jun 07 15:01:07 2015 +0200
@@ -280,7 +280,7 @@
fun proof_local cmd goal_ctxt int after_qed' propss =
Proof.map_context (K goal_ctxt) #>
- Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE
+ Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp cmd NONE
after_qed' (map (pair Thm.empty_binding) propss);
in
@@ -473,7 +473,7 @@
val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (maps (map #1 o #2) asms')
- |> Proof_Context.add_assms_i Assumption.assume_export asms';
+ |> Proof_Context.add_assms Assumption.assume_export asms';
in ctxt' end)
| init (Defines defs) = Context.map_proof (fn ctxt =>
let
@@ -483,7 +483,7 @@
in (t', (b, [(t', ps)])) end);
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (map #1 asms)
- |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
+ |> Proof_Context.add_assms Local_Defs.def_export (map #2 asms);
in ctxt' end)
| init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
--- a/src/Pure/Isar/local_defs.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML Sun Jun 07 15:01:07 2015 +0200
@@ -96,7 +96,7 @@
ctxt
|> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
|> fold Variable.declare_term eqs
- |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
+ |> Proof_Context.add_assms def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
|>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
end;
--- a/src/Pure/Isar/obtain.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Sun Jun 07 15:01:07 2015 +0200
@@ -119,7 +119,7 @@
(*obtain asms*)
val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
- val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
+ val ((_, bind_ctxt), _) = Proof_Context.bind_propp proppss asms_ctxt;
val asm_props = maps (map fst) proppss;
val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss;
--- a/src/Pure/Isar/proof.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sun Jun 07 15:01:07 2015 +0200
@@ -557,8 +557,8 @@
in
-val let_bind = gen_bind Proof_Context.match_bind_i;
-val let_bind_cmd = gen_bind Proof_Context.match_bind;
+val let_bind = gen_bind Proof_Context.match_bind;
+val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd;
end;
@@ -616,8 +616,8 @@
in
-val assm = gen_assume Proof_Context.add_assms_i (K I);
-val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
+val assm = gen_assume Proof_Context.add_assms (K I);
+val assm_cmd = gen_assume Proof_Context.add_assms_cmd Attrib.attribute_cmd;
val assume = assm Assumption.assume_export;
val assume_cmd = assm_cmd Assumption.assume_export;
val presume = assm Assumption.presume_export;
@@ -651,8 +651,8 @@
in
-val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
-val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind;
+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;
end;
@@ -1007,8 +1007,8 @@
init #>
generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp;
-val theorem = global_goal Proof_Context.bind_propp_schematic_i;
-val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
+val theorem = global_goal Proof_Context.bind_propp_schematic;
+val theorem_cmd = global_goal Proof_Context.bind_propp_schematic_cmd;
fun global_qeds arg =
end_proof true arg
@@ -1101,10 +1101,10 @@
in
-val have = gen_have (K I) Proof_Context.bind_propp_i;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp;
-val show = gen_show (K I) Proof_Context.bind_propp_i;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp;
+val have = gen_have (K I) Proof_Context.bind_propp;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp_cmd;
+val show = gen_show (K I) Proof_Context.bind_propp;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Jun 07 15:01:07 2015 +0200
@@ -108,8 +108,8 @@
val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
- val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
- val match_bind_i: bool -> (term list * term) list -> Proof.context -> term list * Proof.context
+ val match_bind: bool -> (term list * term) list -> Proof.context -> term list * Proof.context
+ val match_bind_cmd: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
val read_propp: (string * string list) list list -> Proof.context ->
(term * term list) list list * Proof.context
val cert_propp: (term * term list) list list -> Proof.context ->
@@ -118,13 +118,13 @@
(term * term list) list list * Proof.context
val cert_propp_schematic: (term * term list) list list -> Proof.context ->
(term * term list) list list * Proof.context
- val bind_propp: (string * string list) list list -> Proof.context ->
+ val bind_propp: (term * term list) list list -> Proof.context ->
(term list list * (Proof.context -> Proof.context)) * Proof.context
- val bind_propp_i: (term * term list) list list -> Proof.context ->
+ val bind_propp_cmd: (string * string list) list list -> Proof.context ->
(term list list * (Proof.context -> Proof.context)) * Proof.context
- val bind_propp_schematic: (string * string list) list list -> Proof.context ->
+ val bind_propp_schematic: (term * term list) list list -> Proof.context ->
(term list list * (Proof.context -> Proof.context)) * Proof.context
- val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
+ val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context ->
(term list list * (Proof.context -> Proof.context)) * Proof.context
val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
@@ -143,10 +143,10 @@
val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
string list * Proof.context
val add_assms: Assumption.export ->
- (Thm.binding * (string * string list) list) list ->
+ (Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
- val add_assms_i: Assumption.export ->
- (Thm.binding * (term * term list) list) list ->
+ val add_assms_cmd: Assumption.export ->
+ (Thm.binding * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
@@ -848,7 +848,7 @@
val auto_bind_facts = auto_bind Auto_Bind.facts;
-(* match_bind(_i) *)
+(* match_bind *)
local
@@ -880,8 +880,8 @@
fun read_terms ctxt T =
map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
-val match_bind = gen_bind read_terms;
-val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
+val match_bind = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
+val match_bind_cmd = gen_bind read_terms;
end;
@@ -913,15 +913,15 @@
in
-val read_propp = prep_propp mode_default Syntax.read_props;
-val cert_propp = prep_propp mode_default (map o cert_prop);
+val read_propp = prep_propp mode_default Syntax.read_props;
+val cert_propp = prep_propp mode_default (map o cert_prop);
val read_propp_schematic = prep_propp mode_schematic Syntax.read_props;
val cert_propp_schematic = prep_propp mode_schematic (map o cert_prop);
-val bind_propp = gen_bind_propp mode_default Syntax.read_props;
-val bind_propp_i = gen_bind_propp mode_default (map o cert_prop);
-val bind_propp_schematic = gen_bind_propp mode_schematic Syntax.read_props;
-val bind_propp_schematic_i = gen_bind_propp mode_schematic (map o cert_prop);
+val bind_propp = gen_bind_propp mode_default (map o cert_prop);
+val bind_propp_cmd = gen_bind_propp mode_default Syntax.read_props;
+val bind_propp_schematic = gen_bind_propp mode_schematic (map o cert_prop);
+val bind_propp_schematic_cmd = gen_bind_propp mode_schematic Syntax.read_props;
end;
@@ -1198,7 +1198,7 @@
in
val add_assms = gen_assms bind_propp;
-val add_assms_i = gen_assms bind_propp_i;
+val add_assms_cmd = gen_assms bind_propp_cmd;
end;
--- a/src/Pure/Isar/specification.ML Sun Jun 07 14:36:36 2015 +0200
+++ b/src/Pure/Isar/specification.ML Sun Jun 07 15:01:07 2015 +0200
@@ -372,7 +372,7 @@
in
ctxt'
|> Variable.auto_fixes asm
- |> Proof_Context.add_assms_i Assumption.assume_export
+ |> Proof_Context.add_assms Assumption.assume_export
[((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
|>> (fn [(_, [th])] => th)
end;